Start thinking about caching file context on disk so that cached proof files are available across processes. Here are the possible issues with this implementation:
Only depends on the "libraries hash". Does not depend on CoqPyt version or Coq version.
Hash does not take into account file dependencies. Not sure if that affects correctness.
With that being said this significantly speeds up time for ProofFiles.
For example, the tests go from 94s to 55s on subsequent runs.
Time to run a Proof File for Sudoku.v in the Sudoku repo goes from 199s to 33s.
I think this is important since many files share dependencies even if they are in different projects.
Start thinking about caching file context on disk so that cached proof files are available across processes. Here are the possible issues with this implementation:
With that being said this significantly speeds up time for ProofFiles. For example, the tests go from 94s to 55s on subsequent runs. Time to run a Proof File for Sudoku.v in the Sudoku repo goes from 199s to 33s.
I think this is important since many files share dependencies even if they are in different projects.