Merge branch 'v8.18' into v8.17

CHANGES.md

@@ -11,6 +11,10 @@
  - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
    parsing problem with extra fields in their requests (@ejgallego,
    #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/args.ml

@@ -6,7 +6,8 @@ module Display = struct
 end
 
 type t =
-  { roots : string list  (** workspace root(s) *)
+  { cmdline : Coq.Workspace.CmdLine.t
+  ; roots : string list  (** workspace root(s) *)
   ; files : string list  (** files to compile *)
   ; debug : bool  (** run in debug mode *)
   ; display : Display.t  (** display level *)

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
@@ -21,22 +28,12 @@ let load_plugin plugin_name = Fl_dynload.load_packages [ plugin_name ]
 let plugin_init = List.iter load_plugin
 
 let go args =
-  let { Args.roots; display; debug; files; plugins } = args in
+  let { Args.cmdline; roots; display; debug; files; plugins } = args in
   (* Initialize event callbacks *)
   let io = Output.init display in
   (* Initialize Coq *)
   let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
   let root_state = coq_init ~debug in
-  let cmdline =
-    { Coq.Workspace.CmdLine.coqcorelib =
-        Filename.concat Coq_config.coqlib "../coq-core/"
-    ; coqlib = Coq_config.coqlib
-    ; ocamlpath = None
-    ; vo_load_path = []
-    ; ml_include_path = []
-    ; args = []
-    }
-  in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
   let workspaces =
     List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) roots

compiler/fcc.ml

@@ -2,10 +2,76 @@
 open Cmdliner
 open Fcc_lib
 
-let fcc_main roots display debug plugins files =
-  let args = Args.{ roots; display; files; debug; plugins } in
+let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
+    rload_path load_path =
+  let vo_load_path = rload_path @ load_path in
+  let ml_include_path = [] in
+  let args = [] in
+  let cmdline =
+    { Coq.Workspace.CmdLine.coqlib
+    ; coqcorelib
+    ; ocamlpath
+    ; vo_load_path
+    ; ml_include_path
+    ; args
+    }
+  in
+  let args = Args.{ cmdline; roots; display; files; debug; plugins } in
   Driver.go args
 
+(****************************************************************************)
+(* XXX: Common with coq-lsp.exe *)
+let coqlib =
+  let doc =
+    "Load Coq.Init.Prelude from $(docv); theories and user-contrib should live \
+     there."
+  in
+  Arg.(
+    value & opt string Coq_config.coqlib & info [ "coqlib" ] ~docv:"COQLIB" ~doc)
+
+let coqcorelib =
+  let doc = "Path to Coq plugin directories." in
+  Arg.(
+    value
+    & opt string (Filename.concat Coq_config.coqlib "../coq-core/")
+    & info [ "coqcorelib" ] ~docv:"COQCORELIB" ~doc)
+
+let ocamlpath =
+  let doc = "Path to OCaml's lib" in
+  Arg.(
+    value & opt (some string) None & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc)
+
+let coq_lp_conv ~implicit (unix_path, lp) =
+  { Loadpath.coq_path = Libnames.dirpath_of_string lp
+  ; unix_path
+  ; has_ml = true
+  ; implicit
+  ; recursive = true
+  }
+
+let rload_path : Loadpath.vo_path list Term.t =
+  let doc =
+    "Bind a logical loadpath LP to a directory DIR and implicitly open its \
+     namespace."
+  in
+  Term.(
+    const List.(map (coq_lp_conv ~implicit:true))
+    $ Arg.(
+        value
+        & opt_all (pair dir string) []
+        & info [ "R"; "rec-load-path" ] ~docv:"DIR,LP" ~doc))
+
+let load_path : Loadpath.vo_path list Term.t =
+  let doc = "Bind a logical loadpath LP to a directory DIR" in
+  Term.(
+    const List.(map (coq_lp_conv ~implicit:false))
+    $ Arg.(
+        value
+        & opt_all (pair dir string) []
+        & info [ "Q"; "load-path" ] ~docv:"DIR,LP" ~doc))
+(****************************************************************************)
+
+(* Specific to fcc *)
 let roots : string list Term.t =
   let doc = "Workspace(s) root(s)" in
   Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)
@@ -43,7 +109,9 @@ let fcc_cmd : unit Cmd.t =
   in
   let version = Fleche.Version.server in
   let fcc_term =
-    Term.(const fcc_main $ roots $ display $ debug $ plugins $ file)
+    Term.(
+      const fcc_main $ roots $ display $ debug $ plugins $ file $ coqlib
+      $ coqcorelib $ ocamlpath $ rload_path $ load_path)
   in
   Cmd.(v (Cmd.info "fcc" ~version ~doc ~man) fcc_term)
 

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