From 35b26a321ea79b8780e8f575394f1c04aab57a2b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 May 2024 13:36:26 +0200 Subject: [PATCH] [limits] Don't enable limits automatically on Coq 8.19 or lower unless on a sane branch. This will prevent frustation from users. --- README.md | 2 +- coq/limits.ml | 10 +++++++++- etc/doc/USER_MANUAL.md | 14 ++++++++++++-- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 21caa52f..fc41db6f 100644 --- a/README.md +++ b/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` diff --git a/coq/limits.ml b/coq/limits.ml index 3e640bcb..847962ba 100644 --- a/coq/limits.ml +++ b/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 diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md index eeaa51e2..18234e72 100644 --- a/etc/doc/USER_MANUAL.md +++ b/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,