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.
---
 ide/coq_commands.ml | 1 -
 ide/fake_ide.ml     | 6 +-----
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'ide')

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 5b9ea17ba7..790b427e4c 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -21,7 +21,6 @@ let commands = [
    "Add Printing Let";
    "Add Printing Record";
    "Add Rec LoadPath";
-   "Add Rec ML Path";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
    "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].";
    "Add Relation";
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml
index dfc16d39f3..4292e91252 100644
--- a/ide/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -327,11 +327,7 @@ let main =
     { xml_printer = op; xml_parser = ip } in
   let init () =
     match base_eval_call ~print:false (Xmlprotocol.init None) coq with
-    | Interface.Good id ->
-        let dir = Filename.dirname input_file in
-        let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
-        let eid, tip = add_sentence ~name:"initial" phrase in
-        after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
+    | Interface.Good id -> ()
     | Interface.Fail _ -> error "init call failed" in
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
-- 
cgit v1.2.3