Merge pull request #646 from ejgallego/fix_coqproject_parsing

[workspace] Be more resilient to CoqProject errors.

CHANGES.md

@@ -44,6 +44,8 @@
  - new configuration value `check_only_on_request` which will delay
    checking the document until a request has been made (#629, cc: #24,
    @ejgallego)
+ - fix typo on package.json configuration section (@ejgallego, #645)
+ - be more resilient with invalid _CoqProject files (@ejgallego, #646)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------

README.md

@@ -342,6 +342,8 @@ that have some fixes backported:
   Code extension, Visual Studio Code gets confused and neither of them may
   work. `coq-lsp` will warn about that. You can disable the `VSCoq` extension as
   a workaround.
+- `_CoqProject` file parsing library will often `exit 1` on bad `_CoqProject`
+  files! There is little `coq-lsp` can do here, until upstream fixes this.
 
 ### Troubleshooting
 

compiler/cc.ml

@@ -1,6 +1,7 @@
 (* Compiler context *)
 type t =
   { root_state : Coq.State.t
-  ; workspaces : (string * Coq.Workspace.t) list
+  ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list
+  ; default : Coq.Workspace.t
   ; io : Fleche.Io.CallBack.t
   }

compiler/compile.ml

@@ -2,15 +2,20 @@ open Fleche
 
 let is_in_dir ~dir ~file = CString.is_prefix dir file
 
-let workspace_of_uri ~io ~uri ~workspaces =
+let workspace_of_uri ~io ~uri ~workspaces ~default =
   let file = Lang.LUri.File.to_string_file uri in
   match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
   | None ->
     let lvl = Io.Level.error in
     let message = "file not in workspace: " ^ file in
     Io.Report.message ~io ~lvl ~message;
-    snd (List.hd workspaces)
-  | Some (_, workspace) -> workspace
+    default
+  | Some (_, Error err) ->
+    let lvl = Io.Level.error in
+    let message = "invalid workspace for: " ^ file ^ " " ^ err in
+    Io.Report.message ~io ~lvl ~message;
+    default
+  | Some (_, Ok workspace) -> workspace
 
 (* Improve errors *)
 let save_vo_file ~doc =
@@ -26,14 +31,14 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   Util.format_to_file ~file ~f:Output.pp_diags diags
 
 let compile_file ~cc file =
-  let { Cc.io; root_state; workspaces } = cc in
+  let { Cc.io; root_state; workspaces; default } = cc in
   let lvl = Io.Level.info in
   let message = Format.asprintf "compiling file %s@\n%!" file in
   io.message ~lvl ~message;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> ()
   | Ok uri -> (
-    let workspace = workspace_of_uri ~io ~workspaces ~uri in
+    let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let env = Doc.Env.make ~init:root_state ~workspace in
     let raw = Util.input_all file in
     let () = Theory.create ~io ~env ~uri ~raw ~version:1 in

compiler/driver.ml

@@ -19,7 +19,7 @@ let sanitize_paths message =
     |> replace_test_path "findlib default location: "
 
 let log_workspace ~io (dir, w) =
-  let message, extra = Coq.Workspace.describe w in
+  let message, extra = Coq.Workspace.describe_guess w in
   Fleche.Io.Log.trace "workspace" ("initialized " ^ dir) ~extra;
   let lvl = Fleche.Io.Level.info in
   let message = sanitize_paths message in
@@ -36,11 +36,12 @@ let go args =
   let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
   let root_state = coq_init ~debug in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
+  let default = Coq.Workspace.default ~debug ~cmdline in
   let workspaces =
     List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) roots
   in
   List.iter (log_workspace ~io) workspaces;
-  let cc = Cc.{ root_state; workspaces; io } in
+  let cc = Cc.{ root_state; workspaces; default; io } in
   (* Initialize plugins *)
   plugin_init plugins;
   Compile.compile ~cc files

controller/coq_lsp.ml

@@ -152,7 +152,8 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
     in
 
     (* Core LSP loop context *)
-    let state = { State.root_state; cmdline; workspaces } in
+    let default_workspace = Coq.Workspace.default ~debug ~cmdline in
+    let state = { State.root_state; cmdline; workspaces; default_workspace } in
 
     (* Read workspace state (noop for now) *)
     Cache.read_from_disk ();

controller/lsp_core.ml

@@ -100,7 +100,8 @@ module State = struct
   type t =
     { cmdline : Coq.Workspace.CmdLine.t
     ; root_state : Coq.State.t
-    ; workspaces : (string * Coq.Workspace.t) list
+    ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list
+    ; default_workspace : Coq.Workspace.t (* fail safe *)
     }
 
   open Lsp.Workspace
@@ -128,13 +129,16 @@ module State = struct
     CList.prefix_of String.equal dir_c file_c
 
   let workspace_of_uri ~uri ~state =
-    let { root_state; workspaces; _ } = state in
+    let { root_state; workspaces; default_workspace; _ } = state in
     let file = Lang.LUri.File.to_string_file uri in
     match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
     | None ->
       LIO.logMessage ~lvl:1 ~message:("file not in workspace: " ^ file);
-      (root_state, snd (List.hd workspaces))
-    | Some (_, workspace) -> (root_state, workspace)
+      (root_state, default_workspace)
+    | Some (_, Error _) ->
+      LIO.logMessage ~lvl:1 ~message:("file in errored workspace: " ^ file);
+      (root_state, default_workspace)
+    | Some (_, Ok workspace) -> (root_state, workspace)
 end
 
 let do_changeWorkspaceFolders ~ofn:_ ~state params =
@@ -387,7 +391,7 @@ let do_cancel ~ofn ~params =
 exception Lsp_exit
 
 let log_workspace (dir, w) =
-  let message, extra = Coq.Workspace.describe w in
+  let message, extra = Coq.Workspace.describe_guess w in
   LIO.trace "workspace" ("initialized " ^ dir) ~extra;
   LIO.logMessage ~lvl:3 ~message
 
@@ -402,7 +406,7 @@ let version () =
 
 module Init_effect = struct
   type t =
-    | Success of (string * Coq.Workspace.t) list
+    | Success of (string * (Coq.Workspace.t, string) Result.t) list
     | Loop
     | Exit
 end

controller/lsp_core.mli

@@ -23,7 +23,8 @@ module State : sig
   type t =
     { cmdline : Coq.Workspace.CmdLine.t
     ; root_state : Coq.State.t
-    ; workspaces : (string * Coq.Workspace.t) list
+    ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list
+    ; default_workspace : Coq.Workspace.t  (** fail safe *)
     }
 end
 
@@ -32,7 +33,9 @@ exception Lsp_exit
 (** Lsp special init loop *)
 module Init_effect : sig
   type t =
-    | Success of (string * Coq.Workspace.t) list
+    | Success of (string * (Coq.Workspace.t, string) Result.t) list
+    (* List of workspace roots, + maybe an associated Coq workspace for the
+       path *)
     | Loop
     | Exit
 end

coq/workspace.ml

@@ -244,6 +244,10 @@ let describe
       n_vo n_ml ocamlpath_msg fl_config fl_location
   , extra )
 
+let describe_guess = function
+  | Ok w -> describe w
+  | Error msg -> (msg, "")
+
 (* Require a set of libraries *)
 let load_objs libs =
   let rq_file (dir, from, exp) =
@@ -294,6 +298,9 @@ let apply ~uri
   Declaremods.start_library (dirpath_of_uri ~uri);
   load_objs require_libs
 
+(* This can raise, and will do in incorrect CoqProject files *)
+let dirpath_of_string_exn coq_path = Libnames.dirpath_of_string coq_path
+
 let workspace_from_coqproject ~cmdline ~debug cp_file : t =
   (* Io.Log.error "init" "Parsing _CoqProject"; *)
   let open CoqProject_file in
@@ -306,9 +313,11 @@ let workspace_from_coqproject ~cmdline ~debug cp_file : t =
     ; recursive = true
     ; has_ml = false
     ; unix_path = unix_path.path
-    ; coq_path = Libnames.dirpath_of_string coq_path
+    ; coq_path = dirpath_of_string_exn coq_path
     }
   in
+  (* XXX: [read_project_file] will do [exit 1] on parsing error! Please someone
+     fix upstream!! *)
   let { r_includes; q_includes; ml_includes; extra_args; _ } =
     read_project_file ~warning_fn:(fun _ -> ()) cp_file
   in
@@ -336,8 +345,22 @@ let workspace_from_cmdline ~debug ~cmdline =
   let implicit = true in
   make ~cmdline ~implicit ~kind ~debug
 
-let guess ~debug ~cmdline ~dir =
+let guess ~debug ~cmdline ~dir () =
   let cp_file = Filename.concat dir "_CoqProject" in
   if Sys.file_exists cp_file then
     workspace_from_coqproject ~cmdline ~debug cp_file
   else workspace_from_cmdline ~debug ~cmdline
+
+let guess ~debug ~cmdline ~dir =
+  let { Protect.E.r; feedback } =
+    Protect.eval ~f:(guess ~debug ~cmdline ~dir) ()
+  in
+  ignore feedback;
+  match r with
+  | Protect.R.Interrupted -> Error "Workspace Scanning Interrupted"
+  | Protect.R.Completed (Error (User (_, msg)))
+  | Protect.R.Completed (Error (Anomaly (_, msg))) ->
+    Error (Format.asprintf "Workspace Scanning Errored: %a" Pp.pp_with msg)
+  | Protect.R.Completed (Ok workspace) -> Ok workspace
+
+let default ~debug ~cmdline = workspace_from_cmdline ~debug ~cmdline

coq/workspace.mli

@@ -55,6 +55,8 @@ val hash : t -> int
 (** user message, debug extra data *)
 val describe : t -> string * string
 
+val describe_guess : (t, string) Result.t -> string * string
+
 module CmdLine : sig
   type t =
     { coqlib : string
@@ -67,7 +69,11 @@ module CmdLine : sig
     }
 end
 
-val guess : debug:bool -> cmdline:CmdLine.t -> dir:string -> t
+val guess :
+  debug:bool -> cmdline:CmdLine.t -> dir:string -> (t, string) Result.t
+
+(* Fallback workspace *)
+val default : debug:bool -> cmdline:CmdLine.t -> t
 
 (** [apply libname w] will prepare Coq for a new file [libname] on workspace [w] *)
 val apply : uri:Lang.LUri.File.t -> t -> unit

test/compiler/_CoqProject

@@ -1,4 +1,4 @@
--R proj1 .
+-R . proj1
 
 a.v
 b.v