[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.

2 files changed, 7 insertions, 4 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 95c58b9043..6312bff5f3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2578,7 +2578,8 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Loadpath.coq_path list;
+  ml_load_path   : CUnix.physical_path list;
+  vo_load_path   : Loadpath.vo_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
@@ -2615,7 +2616,7 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; iload_path; require_libs; stm_options } =
+let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } =
 
   let require_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
@@ -2633,7 +2634,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   (* Set load path; important, this has to happen before we declare
      the library below as [Declaremods/Library] will infer the module
      name by looking at the load path! *)
-  List.iter Loadpath.add_coq_path iload_path;
+  List.iter Mltop.add_ml_dir ml_load_path;
+  List.iter Loadpath.add_vo_path vo_load_path;
 
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 841adcf05b..e242225cf2 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -71,7 +71,8 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Loadpath.coq_path list;
+  ml_load_path   : CUnix.physical_path list;
+  vo_load_path   : Loadpath.vo_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,