[fleche] Remove FailedPermanent 8.16 hack

compiler/compile.ml

@@ -34,7 +34,7 @@ let status_of_doc (doc : Doc.t) =
   match doc.completed with
   | Yes _ -> 0
   | Stopped _ -> 2
-  | Failed _ | FailedPermanent _ -> 1
+  | Failed _ -> 1
 
 let compile_file ~cc file : int =
   let { Cc.io; root_state; workspaces; default; token } = cc in

controller/rq_document.ml

@@ -13,7 +13,7 @@ let to_completed = function
   | Fleche.Doc.Completion.Yes range ->
     { Lsp.JFleche.CompletionStatus.status = `Yes; range }
   | Stopped range -> { status = `Stopped; range }
-  | Failed range | FailedPermanent range -> { status = `Failed; range }
+  | Failed range -> { status = `Failed; range }
 
 let request ~token:_ ~doc =
   let { Fleche.Doc.nodes; completed; _ } = doc in

fleche/doc.ml

@@ -237,20 +237,17 @@ module Completion = struct
     | Yes of Lang.Range.t  (** Location of the last token in the document *)
     | Stopped of Lang.Range.t  (** Location of the last valid token *)
     | Failed of Lang.Range.t  (** Critical failure, like an anomaly *)
-    | FailedPermanent of Lang.Range.t
-        (** Temporal Coq hack, avoids any computation *)
 
   let range = function
-    | Yes range | Stopped range | Failed range | FailedPermanent range -> range
+    | Yes range | Stopped range | Failed range -> range
 
   let to_string = function
     | Yes _ -> "fully checked"
     | Stopped _ -> "stopped"
     | Failed _ -> "failed"
-    | FailedPermanent _ -> "refused to create due to Coq parsing bug"
 
   let is_completed = function
-    | Yes _ | Failed _ | FailedPermanent _ -> true
+    | Yes _ | Failed _ -> true
     | _ -> false
 end
 
@@ -292,7 +289,7 @@ type t =
 
 (* Flatten the list of document asts *)
 let asts doc = List.filter_map Node.ast doc.nodes
-let diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes
+let diags doc = List.concat_map Node.diags doc.nodes
 
 (* TOC handling *)
 let rec add_toc_info node toc { Lang.Ast.Info.name; children; _ } =
@@ -380,23 +377,6 @@ let create ~token ~env ~uri ~version ~contents =
         empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed)
   , stats )
 
-(** Create a permanently failed doc, to be removed when we drop 8.16 support *)
-let handle_failed_permanent ~env ~uri ~version ~contents =
-  let completed range = Completion.FailedPermanent range in
-  let loc, message = (None, "Document Failed Permanently due to Coq bugs") in
-  let doc, feedback =
-    error_doc ~loc ~message ~uri ~contents ~version ~env ~completed
-  in
-  let stats = None in
-  let global_stats = Stats.Global.dump () in
-  let nodes =
-    let lines = contents.Contents.lines in
-    process_init_feedback ~lines ~stats ~global_stats env.Env.init feedback
-    @ doc.nodes
-  in
-  let diags_dirty = not (CList.is_empty nodes) in
-  { doc with nodes; diags_dirty }
-
 (** Try to create a doc, if Coq execution fails, create a failed doc with the
     corresponding errors; for now we refine the contents step as to better setup
     the initial document. *)
@@ -448,11 +428,6 @@ let recreate ~token ~doc ~version ~contents =
   let env, uri = (doc.env, doc.uri) in
   handle_doc_creation_exec ~token ~env ~uri ~version ~contents
 
-let create_failed_permanent ~env ~uri ~version ~raw =
-  let completed range = Completion.FailedPermanent range in
-  handle_contents_creation ~env ~uri ~version ~raw ~completed
-    handle_failed_permanent
-
 let recover_up_to_offset ~init_range doc offset =
   Io.Log.trace "prefix"
     (Format.asprintf "common prefix offset found at %d" offset);
@@ -509,7 +484,6 @@ let bump_version ~token ~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 _ ->
     (* re-create the document on failed, as the env may have changed *)
     recreate ~token ~doc ~version ~contents
@@ -1058,7 +1032,7 @@ let check ~io ~token ~target ~doc () =
   | Yes _ ->
     Io.Log.trace "check" "resuming, completed=yes, nothing to do";
     doc
-  | FailedPermanent _ | Failed _ ->
+  | Failed _ ->
     Io.Log.trace "check" "can't resume, failed=yes, nothing to do";
     doc
   | Stopped last_tok ->

fleche/doc.mli

@@ -50,8 +50,6 @@ module Completion : sig
     | Yes of Lang.Range.t  (** Location of the last token in the document *)
     | Stopped of Lang.Range.t  (** Location of the last valid token *)
     | Failed of Lang.Range.t  (** Critical failure, like an anomaly *)
-    | FailedPermanent of Lang.Range.t
-        (** Temporal Coq hack, avoids any computation *)
 
   val is_completed : t -> bool
 end
@@ -139,7 +137,3 @@ val check :
 (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if
     the document completion status is not [Yes] *)
 val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t
-
-(** This is internal, to workaround the Coq multiple-docs problem *)
-val create_failed_permanent :
-  env:Env.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t

fleche/theory.ml

@@ -124,7 +124,7 @@ module Handle = struct
       in
       let handle = { handle with pt_requests = delayed } in
       (handle, pt_ids fullfilled)
-    | Failed _ | FailedPermanent _ -> (handle, Int.Set.empty)
+    | Failed _ -> (handle, Int.Set.empty)
 
   (* trigger pending incremental requests *)
   let update_doc_info ~handle ~(doc : Doc.t) =
@@ -133,8 +133,6 @@ module Handle = struct
     requests
 end
 
-let diags_of_doc doc = List.concat_map Doc.Node.diags doc.Doc.nodes
-
 (* This is temporary for 0.1.9 and our ER project, we need to reify this to a
    general structure *)
 module Register : sig
@@ -173,7 +171,7 @@ end = struct
 end
 
 let send_diags ~io ~token:_ ~doc =
-  let diags = diags_of_doc doc in
+  let diags = Doc.diags doc in
   if List.length diags > 0 || !Config.v.send_diags then
     let uri, version = (doc.uri, doc.version) in
     Io.Report.diagnostics ~io ~uri ~version diags
@@ -290,40 +288,6 @@ let create ~io ~token ~env ~uri ~raw ~version =
   Handle.create ~uri ~doc;
   Check.schedule ~uri
 
-(* Set this to false for < 8.17, 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 ~io ~token ~env ~uri ~raw ~version =
-  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 < 8.17 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
-    let lvl = Io.Level.error in
-    Io.Report.message ~io ~lvl ~message;
-    let doc = Doc.create_failed_permanent ~env ~uri ~raw ~version in
-    Handle.create ~uri ~doc;
-    Check.schedule ~uri)
-  else (
-    tainted := true;
-    create ~io ~token ~env ~uri ~raw ~version)
-
 let change ~io:_ ~token ~(doc : Doc.t) ~version ~raw =
   let uri = doc.uri in
   Io.Log.trace "bump file"
@@ -392,8 +356,7 @@ module Request = struct
     let in_range =
       match doc.completed with
       | Yes _ -> true
-      | Failed range | FailedPermanent range | Stopped range ->
-        Doc.Target.reached ~range (line, col)
+      | Failed range | Stopped range -> Doc.Target.reached ~range (line, col)
     in
     let in_range =
       match version with

test/serlib/genarg/dune

@@ -1,4 +1,5 @@
 ; Eventually we should use the "put binaries in scope feature of Dune"
+
 (rule
  (targets test_roundtrip)
  (deps