We will initially focus on implementing cryptol "Projects" for the purposes of :checking or :proveing all properties in a large collection of modules. The Project concept can be generalized later on if needed.

@yav suggested using https://hackage.haskell.org/package/config-value and https://hackage.haskell.org/package/config-schema for defining the Project configuration file. Initially this would just include a list of modules in the Project. Cryptol should automatically find and load all module dependencies even if they are not explicitly listed. The Project config could also include setting a custom CRYPTOLPATH for where to look for modules.

If we try to load all the modules in a Project at once, we might run into the issue of there being multiple "main" modules which have no name, and this would confuse the cryptol interpreter. We could avoid this by only loading one "main" module at a time, but we should be smart about avoiding unnecessarily re-loading or re-checking common dependencies when possible.

The output of :checking or :proveing a Project should include a report in some machine-readable form (e.g. JSON) so that it can be consumed in CI.

We are solving the "multiple main module" problem by identifying main modules by their filename instead so that there is no conflict.

Once we have the ability to load all modules in a project at once to check or prove their properties, we can save the fingerprint of all the modules (e.g. to a file), so that when we re-run the project we only load in the modules which have changed or whose dependencies have changed. Furthermore, we would only re-prove properties which have a dependency in one of the re-loaded modules.

More details on projects:

• We have a notion of a project "root". This is the directory that all relative paths mentioned in the project configuration are relative to. In other words, it takes the place of the current working directory in resolving relative paths, since we don't want the behavior of running the project to depend on where you happen to invoke it from. In fact, we set the current working directory to the project root at the start of project execution.
• The user can also optionally specify a custom cryptol module search path, equivalent in purpose to the CRYPTOLPATH environment variable. When a custom cryptol path is set, the project behaves as if CRYPTOLPATH was set to that and the --cryptolpath-only flag was turned on, that is, the default cryptol module locations are not searched. If a custom path is not specified, the default paths are used, one of which is the current working directory, which is set to the root as specified above.
• All module dependencies are considered part of the project, even if they are not located under the project folder. We may add some include/exclude mechanism for checking/proving properties of module dependencies if we don't care about the properties in some dependency.
• The project config should explicitly list out at least all the top-level modules of a project (since dependencies should be automatically loaded). If we are adding a project configuration to an existing cryptol codebase with lots of modules, some tool to auto-generate the module list for the first time by scanning the filesystem may be desirable.