From 3f36a86c00bcee2d71d9c326f72da272a484d059 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Feb 2023 19:38:10 +0100 Subject: [PATCH] [fleche] Reject opening multiple Coq documents for buggy Coq versions. Fixes #275 We use a heuristic in the fixed up branches as follows: if the Coq version contains LSP, then we assume the fix has been backported. That should work when doing `opam pin`. --- CHANGES.md | 2 ++ README.md | 32 ++++++++++++++++++++----------- controller/doc_manager.ml | 40 +++++++++++++++++++++++++++++---------- controller/lsp_core.ml | 4 ++-- fleche/doc.ml | 23 ++++++++++++++++++++-- fleche/doc.mli | 6 ++++++ 6 files changed, 82 insertions(+), 25 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 688355044..8a015b241 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -13,6 +13,8 @@ (@artagnon, #277) - Markdown Coq code blocks now must specify "coq" as a language (@ejgallego, #280) + - `coq-lsp` will now reject opening multiple files when the + underlying Coq version is buggy (@ejgallego, fixes #275) # coq-lsp 0.1.4: View --------------------- diff --git a/README.md b/README.md index 8a34d53bd..93bf21ccf 100644 --- a/README.md +++ b/README.md @@ -52,20 +52,30 @@ the best ideas will arise from using `coq-lsp` in your own Coq projects. Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp), don't hesitate to stop by; both users and developers are welcome. -### Troubleshooting +### Troubleshooting and Known Problems -- Most problems can be resolved by restarting `coq-lsp`, in Visual Studio Code, +- Some problems can be resolved by restarting `coq-lsp`, in Visual Studio Code, `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command. -- In VSCode, the "Output" window will have a "Coq LSP Server Events" - channel which should contain some important information. -- As of today, `coq-lsp` may have trouble when more than one file is open at the - same time, this is a problem upstream. For now, you are advised to work on a - single file if this problem appears. This problem is fixed in **Coq 8.18**. +- In VSCode, the "Output" window will have a "Coq LSP Server Events" channel + which should contain some important information; the content of this channel + is controlled by the `Coq LSP > Trace: Server` option. - If you install `coq-lsp` simultaneously with VSCoq, VSCode gets confused and - neither of them may work. `coq-lsp` will warn about that, help with improving - this [issue](https://github.com/ejgallego/coq-lsp/issues/183) is appreciated! -- Some clients may send request completions with a stale document, this will - make completion not to work; we are investigating this issue. + neither of them may work. `coq-lsp` will warn about that. If you know how to + improve this, don't hesitate to get in touch with us. +- VS Code may send request completions with a stale document, this will be fixed + in a new upstream release, c.f. https://github.com/ejgallego/coq-lsp/issues/273 + +#### Working with multiple files + +`coq-lsp` can't work with more than one file at the same time, due to problems +with parsing state management upstream. This was fixed in Coq `master` branch +(to become **Coq 8.18**). + +As this is very inconvenient, we do provide a fixed Coq branch that you can +install using `opam pin`: + +- For Coq 8.17: `opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.17+lsp` +- For Coq 8.16: `opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.16+lsp` ## Features diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index f61cef20e..ea2ff72f9 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -135,7 +135,7 @@ module Handle = struct in let handle = { handle with pt_requests = delayed } in (handle, pt_ids fullfilled) - | Failed _ -> (handle, Int.Set.empty) + | Failed _ | FailedPermanent _ -> (handle, Int.Set.empty) (* trigger pending incremental requests *) let update_doc_info ~handle ~(doc : Fleche.Doc.t) = @@ -164,7 +164,7 @@ module Check = struct let completed ~(doc : Fleche.Doc.t) = match doc.completed with - | Yes _ | Failed _ -> true + | Yes _ | Failed _ | FailedPermanent _ -> true | Stopped _ -> false (* Notification handling; reply is optional / asynchronous *) @@ -216,21 +216,41 @@ let create ~ofmt ~root_state ~workspace ~uri ~raw ~version = send_error_permanent_fail ~ofmt ~uri ~version (Pp.str message) | Interrupted -> () +(* Set this to false for < 8.18, we could parse the version but not worth it. *) +let sane_coq_base_version = true + +let sane_coq_branch = + CString.string_contains ~where:Coq_config.version ~what:"+lsp" + +(* for testing in master, set this to true *) +let force_single_mode = false + +let sane_coq_version = + (sane_coq_base_version || sane_coq_branch) && not force_single_mode + (* Can't wait for the day this goes away *) let tainted = ref false let create ~ofmt ~root_state ~workspace ~uri ~raw ~version = - if !tainted then - (* Warn about Coq bug *) + if !tainted && not sane_coq_version then ( + (* Error due to Coq bug *) let message = "You have opened two or more Coq files simultaneously in the server\n\ - Unfortunately Coq's parser doesn't properly support that setup yet\n\ - If you see some strange parsing errors please close all files but one\n\ - Then restart the coq-lsp server; sorry for the inconveniencies" + Unfortunately Coq's < 8.18 doesn't properly support that setup yet\n\ + You'll need to close all files but one, and restart the server.\n\n\ + Check coq-lsp webpage (Working with multiple files section) for\n\ + instructions on how to install a fixed branch for earlier Coq versions." in - LIO.logMessage ~lvl:2 ~message - else tainted := true; - create ~ofmt ~root_state ~workspace ~uri ~raw ~version + LIO.logMessage ~lvl:1 ~message; + (match + Fleche.Doc.create_failed_permanent ~state:root_state ~uri ~raw ~version + with + | Fleche.Contents.R.Error _e -> () + | Ok doc -> Handle.create ~uri ~doc); + send_error_permanent_fail ~ofmt ~uri ~version (Pp.str message)) + else ( + tainted := true; + create ~ofmt ~root_state ~workspace ~uri ~raw ~version) let change ~ofmt ~(doc : Fleche.Doc.t) ~raw = let uri, version = (doc.uri, doc.version) in diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 8acd92091..e88897c24 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -205,7 +205,7 @@ let request_in_range ~(doc : Fleche.Doc.t) ~version (line, col) = let in_range = match doc.completed with | Yes _ -> true - | Failed range | Stopped range -> + | Failed range | FailedPermanent range | Stopped range -> Fleche.Doc.Target.reached ~range (line, col) in let in_range = @@ -240,7 +240,7 @@ let do_document_request ~params ~handler = let lines = doc.contents.lines in match doc.completed with | Yes _ -> RAction.ok (handler ~lines ~doc) - | Stopped _ | Failed _ -> + | Stopped _ | Failed _ | FailedPermanent _ -> Postpone (PendingRequest.DocRequest { uri; handler }) let do_symbols = do_document_request ~handler:Requests.symbols diff --git a/fleche/doc.ml b/fleche/doc.ml index 776aa9777..71b4467e8 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -154,14 +154,17 @@ module Completion = struct | Yes of Types.Range.t (** Location of the last token in the document *) | Stopped of Types.Range.t (** Location of the last valid token *) | Failed of Types.Range.t (** Critical failure, like an anomaly *) + | FailedPermanent of Types.Range.t + (** Temporal Coq hack, avoids any computation *) let range = function - | Yes range | Stopped range | Failed range -> range + | Yes range | Stopped range | Failed range | FailedPermanent range -> range let to_string = function | Yes _ -> "fully checked" | Stopped _ -> "stopped" | Failed _ -> "failed" + | FailedPermanent _ -> "refused to create due to Coq parsing bug" end (* Private. A doc is a list of nodes for now. The first element in the list is @@ -222,6 +225,21 @@ let create ~state ~workspace ~uri ~version ~raw = | Error e -> Coq.Protect.R.error (Pp.str e) | Ok contents -> create ~state ~workspace ~uri ~version ~contents +let create_failed_permanent ~state ~uri ~version ~raw = + Contents.make ~uri ~raw + |> Contents.R.map ~f:(fun contents -> + let lines = contents.Contents.lines in + let init_loc = init_loc ~uri in + let range = Coq_utils.to_range ~lines init_loc in + { uri + ; contents + ; version + ; root = state + ; nodes = [] + ; diags_dirty = true + ; completed = FailedPermanent range + }) + let recover_up_to_offset ~init_range doc offset = Io.Log.trace "prefix" (Format.asprintf "common prefix offset found at %d" offset); @@ -274,6 +292,7 @@ let bump_version ~version ~(contents : Contents.t) doc = match doc.completed with (* We can do better, but we need to handle the case where the anomaly is when restoring / executing the first sentence *) + | FailedPermanent _ -> doc | Failed _ -> { doc with version @@ -665,7 +684,7 @@ let check ~ofmt ~target ~doc () = | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; doc - | Failed _ -> + | FailedPermanent _ | Failed _ -> Io.Log.trace "check" "can't resume, failed=yes, nothing to do"; doc | Stopped last_tok -> diff --git a/fleche/doc.mli b/fleche/doc.mli index 94aadcf1e..182786f4e 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -45,6 +45,8 @@ module Completion : sig | Yes of Types.Range.t (** Location of the last token in the document *) | Stopped of Types.Range.t (** Location of the last valid token *) | Failed of Types.Range.t (** Critical failure, like an anomaly *) + | FailedPermanent of Types.Range.t + (** Temporal Coq hack, avoids any computation *) end (** A Flèche document is basically a [node list], which is a crude form of a @@ -90,3 +92,7 @@ end (** [check ~ofmt ~target ~doc ()], [target] will have Flèche stop after the point specified there has been reached. *) val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t + +(** This is internal, to workaround the Coq multiple-docs problem *) +val create_failed_permanent : + state:Coq.State.t -> uri:string -> version:int -> raw:string -> t Contents.R.t