RFC: Caching on CI machine

[cpitclaudel]

Our CI takes roughly 12 minutes to run, with approx 2 minutes spent bootstrapping and 10 spent verifying examples. Here's a proposal to make it better:

• Every time we send a query to Z3 and get unsat, we record a hash of that query in a cache file.
• Every time we get a new VC, we check whether we already know that it's unsat from the cache file.

The cache file should also include a Z3 version, and it should survive across CI invocations.

The idea is that in the relatively common case in which a change to F* changes few VCs, we can skip most of the 10 minutes currently spent reverifying everything.

Thoughts?

[BarryBo]

I think we will have much of the infrastructure needed to do this, when we convert the F* build to use Scons instead of make. Scons uses hashes of files instead of timestamps, and records the timestamps of build tools. It also supports use of a disk directory tree as a cache, allowing it to memoize build steps. If the hashes of the inputs and tools match a prior set of hashes, then Scons will copy the result files out of the cache rather than recomputing.

For F* invoking Z3, today, that would be opaque to SCons, since F* invokes Z3 directly, not via a makefile rule.

In Vale, we do have these performance gains, as the Vale compiler generates Dafny source, hands it to Dafny to prove. Scons memoizes the Dafny input and output, skipping the expensive verification in the event that the inputs are unchanged from a prior build.

[cpitclaudel]

I think we will have much of the infrastructure needed to do this, when we convert the F* build to use Scons instead of make. […] For F* invoking Z3, today, that would be opaque to SCons, since F* invokes Z3 directly, not via a makefile rule.

Do we expect to change the way we invoke F*, too? I knew of the plan to move to SCons, but I couldn't/can't see how it will help us here.

[BarryBo]

I think we would have to, in order to make the Z3 programs visible to Scons for memoization. It isn't clear to me whether that's a better approach, than building that caching into F* itself.

[cpitclaudel]

I don't think that would work easily, though: we'd need some form of computed dependencies (the number of queries to Z3 isn't fixed), and we'd be reading from and writing to disk a lot

[BarryBo]

OK, that makes sense then, to do the work in F* itself.

[cpitclaudel]

@nikswamy , @wintersteiger , the recent changes were an implementation of this, right? Can it be closed now?

[nikswamy]

Yes, although the scons work is still applicable and will provide another level of caching, i.e., cache entire fstar invocations.

Maybe we can use this issue to continue to track that part of the work.

[cpitclaudel]

Maybe we can use this issue to continue to track that part of the work.

I'm not sure (it's my bad for mis-titling the issue); this one was very much about caching z3 responses :)