Multiple --cache_dir s for multi-directory compilations

[briangmilnes]

Building a make system (before Fake) when I process a test subdirectory I get appropriate 241 and 247 errors due to having a single --cache_dir to work with.

I checked multiple --cache_dir specs and also treating it like an include, neither work.

This should be a low priority upgrade.

[briangmilnes]

This is a bit worse than I thought. I had to change my rules to $(VALIDATE) || touch $@ when calling libraries in opam. Which we really don't due except via dune looking at fstar and it does not care about it. Even though I have the checked files out there with the right times on them.

[briangmilnes]

Alright this is a project limiting bug. I can't just touch the checked files as they contain data and copying them down to a single cache directory is rather difficult. I can't even get my files that are calling into an opam library to write it's checked file.

If it's not too hard, I could work this one.

[briangmilnes]

As per Nik and Guido mtng today I propose that the minimal configuration version of this is something like:

Each --include'd directory is searched for a single .cache dir. In the fstar opam package we have .cache for .checked files and .hints for .hint file. If we split them then they would best be named .checked and .hints as the simplest form, a single directory .cache.

For each ---include dir, files found in should use the .cache (or others) directory for it or the --cache_dir. This is because to compile within the system you use many includes. A typical Forge include set is 6 includes and a system 15 includes. If an include directory does not exist, a warning could be issued but it should not be a fatal to allow different source directory structures. The language server is currently allowing non-existant include directories without warning.

Writing is to the --cache_dir only, cached files and hints for any file can be found in it.