search

JasonGross / coq-tools

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
MIT License
38 stars 9 forks source link

Incremental compilation #87

Open JasonGross opened 2 years ago

JasonGross commented 2 years ago

It would be nice to have a mode where we kept a pool of coqtop workers and used BackTo to allow us to try multiple changes without recompiling the initial segment of the file. Plausibly we don't want to backtrack across Require statements (bugs exist), which is why having a pool of coqtop workers might be useful (so we could try changing earlier segments without losing state on successful postfixes, maybe?).

ejgallego commented 2 years ago

pyCoq / SerAPI provide this, in both "heavy" and "lightweight" ways

The lightweight way is you just Cancel a document part [and Coq will answer what is not valid anymore] of Fork will create a full new process.

Note by the way that my own internal doc manager for Coq does provide persistance [not sure it is useful here]

ejgallego commented 1 year ago

Update: coq-lsp supports this just by sending updated versions of a .v file to it; it will figure out what not to recompute by itself.

JasonGross commented 1 year ago

Neat! Are all past states cached, so that execution will resume from the longest completed prefix?

ejgallego commented 1 year ago

Yes, for now have not yet implemented any cache-eviction policy, we have researched actually quite a bit on what such strategies would be best, but so far sharing in practice is so high that few users have complained about our very aggresive caching; so improving caching is behind other key milestones.

Any contribution / comment on this front is very welcome.

IMVHO the most interesting point of caching is the interaction with error handling, and I'd love to understand what rules would benefit the minimizer.

For example, as of today, they way we recover failed Qed guarantees that the lemmas after will be able to profit from the cache.

ejgallego commented 1 year ago

For example a goal we have and we are actually close to achieve is going from:

Lemma foo : T.
Proof. by succesful_proof. Qed.

Lemma bar: T.
Proof. by another_proof.  Qed.

to

Lemma foo : T.
Admitted.

Lemma bar: T.
Proof. by another_proof.  Qed.

doesn't re-check bar. As of today it will do because our state is too coarse, but that's gonna be easy to fix once 0.1.8 lands.