[Bug][move-compiler-v2] re-check dependencies in move-prover paths to compiler

[brmataptos]

🐛 Bug

TLDR: If we see strange redundant source file problems, they may result from a conflict between .mv and .move files in compiled packages, since there is still a wild search for .mv files in the parser code (which is shared).

--

We should clean/document up the different kinds of compiler/prover inputs, and name them consistently across prover, move-model, compiler-v2, and compiler-v1. This complication results from the various test frameworks and code paths used.

At a high level, we have:

• primary-target = files to be compiled, warnings generated, tests generated, proved, code generated, etc.
• target = files to be compiled, code generated to support running primary code as needed
  • in test mode, testonly code is included, but test functions are not run
  • no warnings generated (?)
• source-deps = source files to be parsed for declarations to support other activities, no code or local warnings generated.
• bytecode-deps = .mv files to have interface file generated for declarations to support other activities, no local warnings.

After my last "cleanup", things are almost there, but we still have a few potential problems:

• the move-compiler parser distinguishes 2 types:
  • source = primary-target + target (in old world, primary-target is distinguished by package name)
  • deps = source-deps + bytecode-deps
• move-prover only knows about deps, and they are passed to move-model as deps
  • this is probably ok, as we don't need code generated for them

The challenge is that: if there is a .mv file under a directory included in deps, then an interface file will be generated, and might conflict with an existing .move source file if the deps points to a package directory. It may be that deps will be handled correctly. There is code in parser/mod.rs that seem so try to make sure this doesn't happen, but it's possible it doesn't always work.

---

For some more details:

The move-model now takes 3 parameters representing move inputs:

• source / move_sources = primary_target - generate code, run tests, etc.
• source_deps / move_deps = target - generate code but don't compile tests, generate warnings, etc.
• deps = code to use but not generate code for

Calling the parser (V1 front end, Compiler::from_package_paths) these are passed and stored as fields:

• targets: combination of source + source_deps
• deps

The parser is run by calling Compiler: run(), which

• calls generate_interface_files_for_deps(deps, ...), which
  • looks for .mv files in deps and creates .move files for them
  • adds those generated .move files to deps
• calls parse_program(... targets, deps)
  • which drops warnings when parsing deps

Finally, the parser returns a list of the files parsed, their contents, and the parser output.

For move-prover, move-model, and compiler-v2, the move-model then compares this list with its original lists to decide whether to treat something as

• source
• source_dep
• deps
  This code is kind of hairy, and also may hide some bugs.