search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
151 stars 31 forks source link

[fleche] Support Coq Meta Commands Reset and Back #709

Closed ejgallego closed 4 months ago

ejgallego commented 4 months ago

They are pretty easy to support in our model, and actually I can see how they pretty useful to hint the incremental engine to ignore changes!

For example, see this document:


(* Coq code 1 ... *)

Lemma foo : ....

(* Coq code 2 ... *)

Reset foo.

(* Coq code 3 ... *)

In this case, Reset allows us to put a barrier so we can update Coq code 2 at will, and still don't re-check the 3rd code block as it depends on a previous state.

Alizter commented 4 months ago

This is interesting but obviously can't be a recommended practice right?

Another (way more advanced) idea might be for fleche to automatically add Reset comamnds by doing a dependency refinement. That way we can implement tree-like dependencies in a single file rather than having a linear file. How we determine dependencies between vernac statements however is not trivial.

ejgallego commented 4 months ago

This is interesting but obviously can't be a recommended practice right?

Seems like many users still want it, I've realized just now that it is actually pretty useful in some cases.

So as it is trivial to implement, why not?

Another (way more advanced) idea might be for fleche to automatically add Reset comamnds by doing a dependency refinement. That way we can implement tree-like dependencies in a single file rather than having a linear file. How we determine dependencies between vernac statements however is not trivial.

Indeed, that's the idea, but we need to be careful as there is always an overhead (for example Reset will have to search back nodes, with the current list-like structure that we have, that could be improved easily tho)

For now the main point of work is what we have been doing with @SkySkimmer to try to have opaque proofs that don't alter the global state, that would provide crazy speedups in (sound) incremental processing IMHO.

If you are curious about what's needed for this, I think #322 is the first step. (I have a prototype somewhere in private so ping me if you are curious about this)

ejgallego commented 4 months ago

This is ready.

The more I use this, the more I like it. Incrementality gives the commands a new meaning. For example, Reset Initial can be used to have multiple documents in one, all independent.