[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

@@ -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
 ---------------------

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
 

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

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

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 ->

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