Merge pull request #509 from ejgallego/limits

[coq] Support for token-based interruption

README.md

@@ -332,7 +332,7 @@ recommend that if you are installing via opam, you use the following branches
 that have some fixes backported:
 
 - For 8.20: No known problems
-- For 8.19: No known problems
+- For 8.19: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp`
 - For 8.18: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp`
 - For 8.17: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp`
 - For 8.16: `opam pin add coq      https://github.com/ejgallego/coq.git#v8.16+lsp`

coq/limits.ml

@@ -57,8 +57,16 @@ let select = function
   | Coq -> backend := (module Coq)
   | Mp -> backend := (module Mp)
 
+(* Set this to false for 8.19 and lower *)
+let sane_coq_base_version = true
+
+let sane_coq_branch =
+  CString.string_contains ~where:Coq_config.version ~what:"+lsp"
+
+let safe_coq = sane_coq_base_version || sane_coq_branch
+
 let select_best = function
-  | None -> if Mp.available then select Mp else select Coq
+  | None -> if Mp.available && safe_coq then select Mp else select Coq
   | Some backend -> select backend
 
 module Token = struct

etc/doc/USER_MANUAL.md

@@ -79,7 +79,11 @@ not fully completed. Also, you can work with bullets and `coq-lsp`
 will automatically admit unfinished ones, so you can follow the
 natural proof structure.
 
-## Settings
+### Embedded Markdown and LaTeX documents
+
+
+
+## Coq LSP Settings
 
 ### Goal display
 
@@ -91,6 +95,9 @@ A setting to have `coq-lsp` check documents continuously exists.
 
 ## Memory management
 
+You can tell the server to free up memory with the "Coq LSP: Free
+memory" command.
+
 ## Advanced: Multiple workspaces
 
 ## Interrupting coq-lsp
@@ -119,10 +126,13 @@ on Coq <= 8.19 do need to install a version of Coq with the backported
 fixes. See the information about Coq upstream bugs in the README for
 more information about available branches.
 
+`coq-lsp` will reject to enable the new interruption mode by default
+on Coq < 8.20 unless the `lsp` Coq branch version is detected.
+
 ## Advanced incremental tricks
 
 You can use the `Reset $id` and `Back $steps` commands to isolate
-parts of the document from each others in terms of rechecking.
+parts of the document from each other in terms of rechecking.
 
 For example, the command `Reset $id` will make the parts of the
 document after it use the state before the node `id` was found. Thus,