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. --- .../11618-loadpath+split_ml_handling.rst | 9 +++++++++ doc/sphinx/proof-engine/vernacular-commands.rst | 16 ---------------- 2 files changed, 9 insertions(+), 16 deletions(-) create mode 100644 doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst (limited to 'doc') diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst new file mode 100644 index 0000000000..77fa556321 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst @@ -0,0 +1,9 @@ +- **Changed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix.`` + (`#11618 `_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a38c26c2b3..d1f3dcc309 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This -- cgit v1.2.3