Merge pull request #556 from ejgallego/describe_findlib

[coq] Output findlib workspace status in workspace describe.

CHANGES.md

@@ -13,6 +13,8 @@
    #547, reported by @Zimmi48)
  - `fcc` now understands the `--coqlib`, `--coqcorelib`,
    `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, #555)
+ - Describe findlib status in `Workspace.describe`, which is printed
+   in the output windows (@ejgallego, #556)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------

compiler/driver.ml

@@ -4,12 +4,19 @@ let coq_init ~debug =
   let load_plugin = Coq.Loader.plugin_handler None in
   Coq.Init.(coq_init { debug; load_module; load_plugin })
 
+let replace_test_path exp message =
+  let home_re = Str.regexp (exp ^ ".*$") in
+  Str.global_replace home_re "coqlib is at: [TEST_PATH]" message
+
 let sanitize_paths message =
   match Sys.getenv_opt "FCC_TEST" with
   | None -> message
   | Some _ ->
-    let home_re = Str.regexp "coqlib is at: .*$" in
-    Str.global_replace home_re "coqlib is at: [TEST_PATH]" message
+    message
+    |> replace_test_path "coqlib is at: "
+    |> replace_test_path "coqcorelib is at: "
+    |> replace_test_path "findlib config: "
+    |> replace_test_path "findlib default location: "
 
 let log_workspace ~io (dir, w) =
   let message, extra = Coq.Workspace.describe w in

coq/workspace.ml

@@ -159,26 +159,79 @@ let pp_load_path fmt
     (Names.DirPath.to_string coq_path)
     unix_path
 
-let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
+(* This is a bit messy upstream, as -I both extends Coq loadpath and OCAMLPATH
+   loadpath *)
+let findlib_init ~ml_include_path ~ocamlpath =
+  let config, ocamlpath =
+    match ocamlpath with
+    | None -> (None, [])
+    | Some dir -> (Some (Filename.concat dir "findlib.conf"), [ dir ])
+  in
+  let env_ocamlpath = try [ Sys.getenv "OCAMLPATH" ] with Not_found -> [] in
+  let env_ocamlpath = ml_include_path @ env_ocamlpath @ ocamlpath in
+  let ocamlpathsep = if Sys.unix then ":" else ";" in
+  let env_ocamlpath = String.concat ocamlpathsep env_ocamlpath in
+  Findlib.init ~env_ocamlpath ?config ()
+
+let describe
+    { coqlib
+    ; coqcorelib
+    ; ocamlpath
+    ; kind
+    ; vo_load_path
+    ; ml_include_path
+    ; require_libs
+    ; flags = _
+    ; warnings = _
+    ; debug = _
+    } =
   let require_msg =
     String.concat " " (List.map (fun (s, _, _) -> s) require_libs)
   in
   let n_vo = List.length vo_load_path in
   let n_ml = List.length ml_include_path in
+  let ocamlpath_msg =
+    Option.cata
+      (fun op -> "was overrident to " ^ op)
+      "wasn't overriden" ocamlpath
+  in
+  (* We need to do this in order for the calls to Findlib to make sense, but
+     really need to modify this *)
+  findlib_init ~ml_include_path ~ocamlpath;
+  let fl_packages = Findlib.list_packages' () in
+  let fl_config = Findlib.config_file () in
+  let fl_location = Findlib.default_location () in
+  let fl_paths = Findlib.search_path () in
   let extra =
-    Format.asprintf "@[vo_paths:@\n @[<v>%a@]@\nml_paths:@\n @[<v>%a@]@]"
+    Format.asprintf
+      "@[vo_paths:@\n\
+      \ @[<v>%a@]@\n\
+       ml_paths:@\n\
+      \ @[<v>%a@]@\n\
+       findlib_paths:@\n\
+      \ @[<v>%a@]@\n\
+       findlib_packages:@\n\
+      \ @[<v>%a@]@]"
       (Format.pp_print_list pp_load_path)
       vo_load_path
       Format.(pp_print_list pp_print_string)
       ml_include_path
+      Format.(pp_print_list pp_print_string)
+      fl_paths
+      Format.(pp_print_list pp_print_string)
+      fl_packages
   in
   ( Format.asprintf
       "@[Configuration loaded from %s@\n\
       \ - coqlib is at: %s@\n\
+      \   + coqcorelib is at: %s@\n\
       \ - Modules [%s] will be loaded by default@\n\
       \ - %d Coq path directory bindings in scope; %d Coq plugin directory \
-       bindings in scope@]"
-      kind coqlib require_msg n_vo n_ml
+       bindings in scope@\n\
+      \ - ocamlpath %s@\n\
+      \   + findlib config: %s@\n\
+      \   + findlib default location: %s@]" kind coqlib coqcorelib require_msg
+      n_vo n_ml ocamlpath_msg fl_config fl_location
   , extra )
 
 (* Require a set of libraries *)
@@ -209,20 +262,6 @@ let dirpath_of_uri ~uri =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-(* This is a bit messy upstream, as -I both extends Coq loadpath and OCAMLPATH
-   loadpath *)
-let findlib_init ~ml_include_path ~ocamlpath =
-  let config, ocamlpath =
-    match ocamlpath with
-    | None -> (None, [])
-    | Some dir -> (Some (Filename.concat dir "findlib.conf"), [ dir ])
-  in
-  let env_ocamlpath = try [ Sys.getenv "OCAMLPATH" ] with Not_found -> [] in
-  let env_ocamlpath = ml_include_path @ env_ocamlpath @ ocamlpath in
-  let ocamlpathsep = if Sys.unix then ":" else ";" in
-  let env_ocamlpath = String.concat ocamlpathsep env_ocamlpath in
-  Findlib.init ~env_ocamlpath ?config ()
-
 (* NOTE: Use exhaustive match below to avoid bugs by skipping fields *)
 let apply ~uri
     { coqlib = _

test/compiler/run.t

@@ -5,15 +5,23 @@ Describe the project
   $ fcc --root proj1
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
 
 Compile a single file
   $ fcc --root proj1 proj1/a.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/a.v
 
   $ ls proj1
@@ -29,8 +37,12 @@ Compile a dependent file
   $ fcc --root proj1 proj1/b.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/b.v
 
   $ ls proj1
@@ -46,8 +58,12 @@ Compile both files
   $ fcc --root proj1 proj1/a.v proj1/b.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/a.v
 
   [message] compiling file proj1/b.v
@@ -65,8 +81,12 @@ Compile a dependent file without the dep being built
   $ fcc --root proj1 proj1/b.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/b.v
 
   $ ls proj1
@@ -107,12 +127,20 @@ Use two workspaces
   $ fcc --root proj1 --root proj2 proj1/a.v proj2/b.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/a.v
 
   [message] compiling file proj2/b.v
@@ -126,8 +154,12 @@ Load the example plugin
   $ fcc --plugin=coq-lsp.plugin.example --root proj1 proj1/a.v
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope
+   - ocamlpath wasn't overriden
+     + coqlib is at: [TEST_PATH]
+     + coqlib is at: [TEST_PATH]
   [message] compiling file proj1/a.v
 
   [example plugin] file checking for proj1/a.v was completed