[args] [coq] Allow to set ocamlpath and findlib init file separately.

This is needed for example in the JS case, likely this will help with
the Coq Platform Windows Installer.

compiler/fcc.ml

@@ -3,14 +3,15 @@ open Cmdliner
 open Fcc_lib
 
 let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
-    ocamlpath rload_path load_path require_libraries no_vo max_errors
-    coq_diags_level =
+    findlib_config ocamlpath rload_path load_path require_libraries no_vo
+    max_errors coq_diags_level =
   let vo_load_path = rload_path @ load_path in
   let ml_include_path = [] in
   let args = [] in
   let cmdline =
     { Coq.Workspace.CmdLine.coqlib
     ; coqcorelib
+    ; findlib_config
     ; ocamlpath
     ; vo_load_path
     ; ml_include_path
@@ -100,8 +101,8 @@ let fcc_cmd : int Cmd.t =
     let open Coq.Args in
     Term.(
       const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
-      $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from
-      $ no_vo $ max_errors $ coq_diags_level)
+      $ coqlib $ coqcorelib $ findlib_config $ ocamlpath $ rload_paths
+      $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

controller/coq_lsp.ml

@@ -80,8 +80,8 @@ let rec lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug =
     L.trace "read_request" "error: %s" err;
     lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug
 
-let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
-    require_libraries delay int_backend =
+let lsp_main bt coqcorelib coqlib findlib_config ocamlpath vo_load_path
+    ml_include_path require_libraries delay int_backend =
   Coq.Limits.select_best int_backend;
   Coq.Limits.start ();
 
@@ -113,6 +113,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
   let cmdline =
     { Coq.Workspace.CmdLine.coqcorelib
     ; coqlib
+    ; findlib_config
     ; ocamlpath
     ; vo_load_path
     ; ml_include_path
@@ -199,8 +200,8 @@ let lsp_cmd : unit Cmd.t =
     v
       (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man)
       Term.(
-        const lsp_main $ bt $ coqcorelib $ coqlib $ ocamlpath $ vo_load_path
-        $ ml_include_path $ ri_from $ delay $ int_backend))
+        const lsp_main $ bt $ coqcorelib $ coqlib $ findlib_config $ ocamlpath
+        $ vo_load_path $ ml_include_path $ ri_from $ delay $ int_backend))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in

coq/args.ml

@@ -24,10 +24,17 @@ let coqcorelib =
     & opt string (Filename.concat Coq_config.coqlib "../coq-core/")
     & info [ "coqcorelib" ] ~docv:"COQCORELIB" ~doc)
 
+let findlib_config =
+  let doc = "Override findlib's config file" in
+  Arg.(
+    value
+    & opt (some string) None
+    & info [ "findlib_config" ] ~docv:"OCAMLFIND_CONF" ~doc)
+
 let ocamlpath =
-  let doc = "Path to OCaml's lib" in
+  let doc = "Extra Paths to OCaml's libraries" in
   Arg.(
-    value & opt (some string) None & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc)
+    value & opt (list string) [] & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc)
 
 let coq_lp_conv ~implicit (unix_path, lp) =
   { Loadpath.coq_path = Libnames.dirpath_of_string lp

coq/args.mli

@@ -9,7 +9,8 @@ open Cmdliner
 
 val coqlib : String.t Term.t
 val coqcorelib : String.t Term.t
-val ocamlpath : String.t option Term.t
+val findlib_config : String.t option Term.t
+val ocamlpath : String.t list Term.t
 val rload_paths : Loadpath.vo_path List.t Term.t
 val qload_paths : Loadpath.vo_path List.t Term.t
 val debug : Bool.t Term.t

coq/workspace.ml

@@ -68,7 +68,8 @@ end
 type t =
   { coqlib : string
   ; coqcorelib : string
-  ; ocamlpath : string option
+  ; findlib_config : string option
+  ; ocamlpath : string list
   ; vo_load_path : Loadpath.vo_path list
   ; ml_include_path : string list
   ; require_libs : Require.t list
@@ -125,7 +126,8 @@ module CmdLine = struct
   type t =
     { coqlib : string
     ; coqcorelib : string
-    ; ocamlpath : string option
+    ; findlib_config : string option
+    ; ocamlpath : string list
     ; vo_load_path : Loadpath.vo_path list
     ; ml_include_path : string list
     ; args : string list
@@ -140,6 +142,7 @@ let mk_require_from (from, library) =
 let make ~cmdline ~implicit ~kind ~debug =
   let { CmdLine.coqcorelib
       ; coqlib
+      ; findlib_config
       ; ocamlpath
       ; args
       ; ml_include_path
@@ -178,6 +181,7 @@ let make ~cmdline ~implicit ~kind ~debug =
   let ml_include_path = dft_ml_include_path @ ml_include_path in
   { coqlib
   ; coqcorelib
+  ; findlib_config
   ; ocamlpath
   ; vo_load_path
   ; ml_include_path
@@ -196,12 +200,8 @@ let pp_load_path fmt
 
 (* 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 findlib_init ~ml_include_path ?findlib_config ~ocamlpath () =
+  let config = findlib_config 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
@@ -211,6 +211,7 @@ let findlib_init ~ml_include_path ~ocamlpath =
 let describe
     { coqlib
     ; coqcorelib
+    ; findlib_config
     ; ocamlpath
     ; kind
     ; vo_load_path
@@ -227,13 +228,11 @@ let describe
   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
+    "added ocamlpaths: [" ^ String.concat "|" 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;
+  findlib_init ~ml_include_path ?findlib_config ~ocamlpath ();
   let fl_packages = Findlib.list_packages' () in
   let fl_config = Findlib.config_file () in
   let fl_location = Findlib.default_location () in
@@ -311,6 +310,7 @@ let dirpath_of_uri ~uri =
 let apply ~intern ~uri
     { coqlib = _
     ; coqcorelib = _
+    ; findlib_config
     ; ocamlpath
     ; vo_load_path
     ; ml_include_path
@@ -324,7 +324,7 @@ let apply ~intern ~uri
   Flags.apply flags;
   Warning.apply warnings;
   List.iter Mltop.add_ml_dir ml_include_path;
-  findlib_init ~ml_include_path ~ocamlpath;
+  findlib_init ~ml_include_path ?findlib_config ~ocamlpath ();
   List.iter Loadpath.add_vo_path vo_load_path;
   Declaremods.start_library (dirpath_of_uri ~uri);
   load_objs ~intern require_libs

coq/workspace.mli

@@ -46,7 +46,10 @@ end
 type t = private
   { coqlib : string
   ; coqcorelib : string
-  ; ocamlpath : string option
+  ; findlib_config :
+      string option (* Path to findlib config file, if [None], default *)
+  ; ocamlpath :
+      string list (* extra ocamlpath paths, for example for local plugins *)
   ; vo_load_path : Loadpath.vo_path list
         (** List of -R / -Q flags passed to Coq, usually theories we depend on *)
   ; ml_include_path : string list
@@ -78,7 +81,8 @@ module CmdLine : sig
   type t =
     { coqlib : string
     ; coqcorelib : string
-    ; ocamlpath : string option
+    ; findlib_config : string option
+    ; ocamlpath : string list
     ; vo_load_path : Loadpath.vo_path list
     ; ml_include_path : string list
     ; args : string list

petanque/json_shell/shell.ml

@@ -6,7 +6,8 @@ let init_coq ~debug =
 let cmdline : Coq.Workspace.CmdLine.t =
   { coqlib = Coq_config.coqlib
   ; coqcorelib = Filename.concat Coq_config.coqlib "../coq-core"
-  ; ocamlpath = None
+  ; findlib_config = None
+  ; ocamlpath = []
   ; vo_load_path = []
   ; ml_include_path = []
   ; args = []

test/compiler/basic/run.t

@@ -8,7 +8,7 @@ Describe the project
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
 
@@ -19,7 +19,7 @@ Compile a single file, don't generate a `.vo` file:
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -35,7 +35,7 @@ Compile a single file, generate a .vo file
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -55,7 +55,7 @@ Compile a dependent file
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
@@ -75,7 +75,7 @@ Compile both files
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -96,7 +96,7 @@ Compile a dependent file without the dep being built
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/b.v
@@ -114,15 +114,15 @@ Compile a dependent file without the dep being built
       "end": { "line": 0, "character": 9 }
     },
     "severity": 1,
-    "message": "Cannot find a physical path bound to logical path a."
+    "message": "Cannot find a physical path bound to logical path\na.\nRaised at Exninfo.iraise in file \"vendor/coq/clib/exninfo.ml\", line 79, characters 4-11\nCalled from CList.map in file \"vendor/coq/clib/cList.ml\", line 309, characters 21-24\nCalled from Synterp.synterp_require in file \"vendor/coq/vernac/synterp.ml\", line 305, characters 16-36\nCalled from Vernacentries.vernac_require in file \"vendor/coq/vernac/vernacentries.ml\", line 1406, characters 24-72\nCalled from VernacControl.under_control in file \"vendor/coq/vernac/vernacControl.ml\", line 122, characters 14-18\nCalled from Coq__Utils.with_control in file \"coq/utils.ml\", line 52, characters 4-79\nCalled from Coq__Interp.Require.interp in file \"coq/interp.ml\", line 41, characters 13-48\nCalled from Memprof_limits__Masking.with_resource in file \"src/masking.ml\", line 54, characters 4-11\nRe-raised at Memprof_limits__Masking.with_resource in file \"src/masking.ml\", line 67, characters 10-44\nCalled from Memprof_limits__Limits_callbacks.result_of_token in file \"src/limits_callbacks.ml\", line 20, characters 8-12\nCalled from Coq__Protect.eval_exn in file \"coq/protect.ml\", line 37, characters 8-32\n"
   }
   {
     "range": {
       "start": { "line": 1, "character": 17 },
       "end": { "line": 1, "character": 21 }
     },
     "severity": 1,
-    "message": "The reference a.aa was not found in the current environment."
+    "message": "The reference a.aa was not found in the current\nenvironment.\nRaised at Stdlib__Map.Make.find in file \"map.ml\", line 137, characters 10-25\nCalled from Nametab.Make.find_node in file \"vendor/coq/library/nametab.ml\", line 296, characters 14-34\nCalled from Nametab.Make.locate in file \"vendor/coq/library/nametab.ml\", line 299, characters 16-33\nCalled from Nametab.locate_extended_nowarn in file \"vendor/coq/library/nametab.ml\" (inlined), line 620, characters 13-45\nCalled from Nametab.locate_extended in file \"vendor/coq/library/nametab.ml\", line 625, characters 13-39\nCalled from Constrintern.intern_extended_global_of_qualid in file \"vendor/coq/interp/constrintern.ml\", line 1200, characters 10-37\nCalled from Constrintern.intern_qualid in file \"vendor/coq/interp/constrintern.ml\", line 1352, characters 8-44\nCalled from Constrintern.intern_applied_reference in file \"vendor/coq/interp/constrintern.ml\", line 1472, characters 32-76\nRe-raised at Exninfo.iraise in file \"vendor/coq/clib/exninfo.ml\", line 81, characters 4-38\nCalled from Constrintern.internalize.intern.(fun) in file \"vendor/coq/interp/constrintern.ml\", line 2147, characters 10-124\nCalled from Constrintern.interp_constr_evars_gen_impls in file \"vendor/coq/interp/constrintern.ml\", line 2733, characters 10-53\nCalled from ComDefinition.interp_definition in file \"vendor/coq/vernac/comDefinition.ml\", line 99, characters 31-90\nCalled from ComDefinition.do_definition in file \"vendor/coq/vernac/comDefinition.ml\", line 127, characters 4-93\nCalled from Vernacentries.vernac_definition in file \"vendor/coq/vernac/vernacentries.ml\", line 676, characters 6-154\nCalled from Vernactypes.vtmodifyprogram.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 197, characters 30-40\nCalled from Vernactypes.typed_vernac.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 170, characters 65-71\nCalled from Vernactypes.run.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 164, characters 15-32\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 126, characters 16-23\nCalled from Vernactypes.OpaqueAccess.runner.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 114, characters 30-34\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 125, characters 14-100\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 126, characters 16-23\nCalled from Vernactypes.Proof.runner.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 69, characters 30-34\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 125, characters 14-100\nCalled from Vernactypes.Prog.runner.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 30, characters 20-24\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 124, characters 12-173\nCalled from Vernactypes.combine_runners.(fun) in file \"vendor/coq/vernac/vernactypes.ml\", line 124, characters 12-173\nCalled from Vernactypes.run in file \"vendor/coq/vernac/vernactypes.ml\", line 163, characters 14-96\nCalled from Vernacinterp.interp_expr_core in file \"vendor/coq/vernac/vernacinterp.ml\", line 80, characters 60-157\nCalled from Vernacinterp.interp_expr in file \"vendor/coq/vernac/vernacinterp.ml\", line 49, characters 19-121\nCalled from VernacControl.under_control in file \"vendor/coq/vernac/vernacControl.ml\", line 122, characters 14-18\nCalled from Vernacinterp.interp_control_gen in file \"vendor/coq/vernac/vernacinterp.ml\", line 36, characters 4-137\nCalled from Flags.with_modified_ref in file \"vendor/coq/lib/flags.ml\", line 17, characters 14-17\nRe-raised at Exninfo.iraise in file \"vendor/coq/clib/exninfo.ml\", line 81, characters 4-38\nCalled from Vernacinterp.interp_gen in file \"vendor/coq/vernac/vernacinterp.ml\", line 146, characters 16-41\nRe-raised at Exninfo.iraise in file \"vendor/coq/clib/exninfo.ml\", line 81, characters 4-38\nCalled from Vernacinterp.interp in file \"vendor/coq/vernac/vernacinterp.ml\", line 160, characters 15-115\nCalled from Coq__Interp.coq_interp in file \"coq/interp.ml\", line 21, characters 2-37\nCalled from Memprof_limits__Masking.with_resource in file \"src/masking.ml\", line 54, characters 4-11\nRe-raised at Memprof_limits__Masking.with_resource in file \"src/masking.ml\", line 67, characters 10-44\nCalled from Memprof_limits__Limits_callbacks.result_of_token in file \"src/limits_callbacks.ml\", line 20, characters 8-12\nCalled from Coq__Protect.eval_exn in file \"coq/protect.ml\", line 37, characters 8-32\n"
   }
 
 Compile a file with all messages:
@@ -133,7 +133,7 @@ Compile a file with all messages:
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -144,7 +144,7 @@ Compile a file with all messages:
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -174,22 +174,27 @@ Use two workspaces
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
   [message] compiling file proj2/b.v
   fcc: internal error, uncaught exception:
        Sys_error("proj2/b.v: No such file or directory")
-
+       Raised by primitive operation at Stdlib.open_in_gen in file "stdlib.ml", line 405, characters 28-54
+       Called from Coq__Compat.Ocaml_414.In_channel.with_open in file "coq/compat.ml", line 25, characters 15-24
+       Called from Fcc_lib__Compile.compile_file in file "compiler/compile.ml", line 44, characters 47-75
+       Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
+       Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
+       Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
   [125]
 
 Load the example plugin
@@ -199,7 +204,7 @@ Load the example plugin
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -212,7 +217,7 @@ Load the astdump plugin
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v
@@ -237,7 +242,7 @@ We do the same for the goaldump plugin:
      + coqcorelib is at: [TEST_PATH]
    - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
-   - ocamlpath wasn't overriden
+   - ocamlpath added ocamlpaths: []
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] compiling file proj1/a.v