wip: coq interruption

[gares]

requires sel branch

There is a big issue, namely that Coq is not thread safe (nor purely functional). Scenario: the execution manager (thread) is running on a sentence: it installed a global state and is possibly even modifying it in place before snapshotting it back; at the same time the lsp manager gets a request, like hover or query or completion, that currently installs a Coq state and run some code. Things can go south in hard to debug ways.

So, if we follow the path of running "coq" in a thread and the "language server" in another one, all calls to (non purely functional) Coq APIs have to go through a single point in the execution manager and be queued, or interleaved, taking care of properly handling the global state.

[gares]

CC @rtetley, when you have a minute, could you please add a stop button to the UI ?

[Durbatuluk1701]

Along with a stop button could we have a key binding to interrupt as well

[gares]

After some thinking the plan could be:

• rework the source tree to use (implicit_transitive_deps false) in dune-project and have all Rocq calls / types in a dedicated library rocq_enclave. All code outside the enclave should not list coq-core.* in the dune file, hence it cannot call Rocq APIs. In this way we precisely control what we call
• make sure that Rocq calls are made in a single thread and serialized one after the other
  • with an API to interrupt, possibly using memprof_limits
  • use the same priorities we use for sel in the API: if a call has higher priority interrupt the running one
  • bonus: if a call has higher priority interrupt the running one (after say 0.1) and run the high prio one, then restart the interrupted one

This includes all Rocq calls, the queries, the parser, etc

Some Rocq code may not need this, being pure, but it is not so clear how to know it and ensure it Rocq side. Eg Search seems pure, but prints the results using the current notations, so it is not really pure.

[rtetley]

CC @rtetley, when you have a minute, could you please add a stop button to the UI ?

Done

Along with a stop button could we have a key binding to interrupt as well

I created a command that you can call from the palette. What default keybinding should we use ?

[Durbatuluk1701]

I know it has been previously suggested that if you have an in-progress proof and input the "Step Backward" key bind it should be interpreted as "Interrupt", so that is a possibility.

I also think maybe given that we have commands bound to up, down, and right arrow keys, maybe left arrow key could be "Interrupt"?