diff --git a/CHANGES.md b/CHANGES.md index 09ac8e97..1e201939 100644 --- a/CHANGES.md +++ b/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 ------------------------------- diff --git a/README.md b/README.md index 33672ea0..e73d5870 100644 --- a/README.md +++ b/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 diff --git a/compiler/cc.ml b/compiler/cc.ml index 82091f3a..828e2bd4 100644 --- a/compiler/cc.ml +++ b/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 } diff --git a/compiler/compile.ml b/compiler/compile.ml index 9f066508..4b16b1f5 100644 --- a/compiler/compile.ml +++ b/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 diff --git a/compiler/driver.ml b/compiler/driver.ml index d67a9b21..5f78127d 100644 --- a/compiler/driver.ml +++ b/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 diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 19dc9d11..993aaa0d 100644 --- a/controller/coq_lsp.ml +++ b/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 (); diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 943a0075..2ab779e3 100644 --- a/controller/lsp_core.ml +++ b/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 diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli index c42f7d88..14bb111f 100644 --- a/controller/lsp_core.mli +++ b/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 diff --git a/coq/workspace.ml b/coq/workspace.ml index 9eddf563..947ea349 100644 --- a/coq/workspace.ml +++ b/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 diff --git a/coq/workspace.mli b/coq/workspace.mli index b2fcd706..b5a4f2cd 100644 --- a/coq/workspace.mli +++ b/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 diff --git a/test/compiler/_CoqProject b/test/compiler/_CoqProject index 77011d3b..9303b093 100644 --- a/test/compiler/_CoqProject +++ b/test/compiler/_CoqProject @@ -1,4 +1,4 @@ --R proj1 . +-R . proj1 a.v b.v