From b44fce96503c39a4306a627e5ba992634728954d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 14 Feb 2020 00:49:01 +0100
Subject: [loadpath] Rework and simplify ML loadpath handling

This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.

This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.

The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.

We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.

Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]

In terms of vernaculars the changes are:

- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
  form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.

We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
---
 toplevel/ccompile.ml | 15 ++++++++-------
 toplevel/coqargs.ml  | 17 +++++++----------
 toplevel/coqargs.mli |  6 +++---
 toplevel/coqinit.ml  | 51 ++++++++++++++++++++-------------------------------
 toplevel/coqinit.mli |  4 ++--
 toplevel/coqtop.ml   |  6 +++---
 6 files changed, 43 insertions(+), 56 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index dceb811d66..f75a706041 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -104,7 +104,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
@@ -129,8 +129,8 @@ let compile opts copts ~echo ~f_in ~f_out =
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VoDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
@@ -181,8 +181,8 @@ let compile opts copts ~echo ~f_in ~f_out =
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VioDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
@@ -252,8 +252,9 @@ let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling
      process happens outside of the STM *)
   if copts.vio_files <> [] || copts.vio_tasks <> [] then
-    let iload_path = build_load_path opts in
-    List.iter Loadpath.add_coq_path iload_path;
+    let ml_lp, vo_lp = build_load_path opts in
+    List.iter Mltop.add_ml_dir ml_lp;
+    List.iter Loadpath.add_vo_path vo_lp;
 
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 949a13974c..24cfecd057 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -70,8 +70,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : string list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -164,14 +164,13 @@ let default = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }}
+  { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
 
 let add_vo_include opts unix_path coq_path implicit =
   let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
   { opts with pre = { opts.pre with vo_includes = {
-        recursive = true;
-        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }}
+        unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
   { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
@@ -582,9 +581,7 @@ let prelude_data = "Prelude", Some "Coq", Some false
 let require_libs opts =
   if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
-let cmdline_load_path opts =
-  opts.pre.ml_includes @ opts.pre.vo_includes
-
 let build_load_path opts =
-  (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @
-  cmdline_load_path opts
+  let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in
+  ml_path @ opts.pre.ml_includes ,
+  vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index aba6811f43..88de48967a 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -46,8 +46,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : CUnix.physical_path list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -83,4 +83,4 @@ val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * strin
 val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
-val build_load_path : t -> Loadpath.coq_path list
+val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7f3d4b570f..ce054d2af2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,34 +51,22 @@ let load_rcfile ~rcfile ~state =
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
 
-(* Recursively puts `.v` files in the LoadPath if -nois was not passed *)
+(* Recursively puts `.v` files in the LoadPath *)
 let build_stdlib_vo_path ~unix_path ~coq_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true }
-  }
-
-let build_stdlib_ml_path ~dir =
-  let open Loadpath in
-  { recursive = true
-  ; path_spec = MlPath dir
-  }
+  { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
 
 let build_userlib_path ~unix_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath {
-        unix_path;
-        coq_path = Libnames.default_root_prefix;
-        has_ml = AddRecML;
-        implicit = false;
-      }
+  { unix_path
+  ; coq_path = Libnames.default_root_prefix
+  ; has_ml = true
+  ; implicit = false
+  ; recursive = true
   }
 
 let ml_path_if c p =
-  let open Loadpath in
-  let f x = { recursive = false; path_spec = MlPath x } in
-  if c then List.map f p else []
+  if c then p else []
 
 (* LoadPath for developers *)
 let toplevel_init_load_path () =
@@ -97,16 +85,19 @@ let libs_init_load_path () =
   let coqpath = Envars.coqpath in
   let coq_path = Names.DirPath.make [Libnames.coq_root] in
 
+  (* ML includes *)
+  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in
+  List.map fst plugins_dirs,
+
   (* current directory (not recursively!) *)
-  [ { recursive = false;
-      path_spec = VoPath { unix_path = ".";
-                           coq_path = Libnames.default_root_prefix;
-                           implicit = false;
-                           has_ml = AddTopML }
+  [ { unix_path = "."
+    ; coq_path = Libnames.default_root_prefix
+    ; implicit = false
+    ; has_ml = true
+    ; recursive = false
     } ] @
 
   (* then standard library *)
-  [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
   [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
@@ -120,10 +111,8 @@ let libs_init_load_path () =
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
-  let open Loadpath in
-  let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl]))
+    Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl])
   in
-    Loadpath.add_coq_path (lp (Envars.coqlib ()));
-    List.iter add_subdir Coq_config.all_src_dirs
+  Mltop.add_ml_dir (Envars.coqlib ());
+  List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index f3a007d987..f099173808 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Loadpath.coq_path list
+val toplevel_init_load_path : unit -> CUnix.physical_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : unit -> Loadpath.coq_path list
+val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1ea48ee766..1e6b1023fe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -226,7 +226,7 @@ let init_execution opts custom_init =
   Spawned.init_channels ();
   if opts.post.memory_stat then at_exit print_memory_stat;
   let top_lp = Coqinit.toplevel_init_load_path () in
-  List.iter Loadpath.add_coq_path top_lp;
+  List.iter Mltop.add_ml_dir top_lp;
   CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
@@ -281,14 +281,14 @@ let init_document opts =
   *)
   (* Next line allows loading .vos files when in interactive mode *)
   Flags.load_vos_libraries := true;
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             iload_path; require_libs; stm_options;
+             ml_load_path; vo_load_path; require_libs; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
-- 
cgit v1.2.3