aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst9
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst16
-rw-r--r--ide/coq_commands.ml1
-rw-r--r--ide/fake_ide.ml6
-rw-r--r--stm/stm.ml43
-rw-r--r--stm/stm.mli46
-rw-r--r--test-suite/ide/debug_ltac.fake1
-rw-r--r--test-suite/ide/undo002.fake1
-rw-r--r--toplevel/ccompile.ml15
-rw-r--r--toplevel/coqargs.ml17
-rw-r--r--toplevel/coqargs.mli6
-rw-r--r--toplevel/coqinit.ml51
-rw-r--r--toplevel/coqinit.mli4
-rw-r--r--toplevel/coqtop.ml6
-rw-r--r--vernac/g_vernac.mlg16
-rw-r--r--vernac/loadpath.ml56
-rw-r--r--vernac/loadpath.mli29
-rw-r--r--vernac/mltop.ml5
-rw-r--r--vernac/mltop.mli2
-rw-r--r--vernac/ppvernac.ml14
-rw-r--r--vernac/vernacentries.ml19
-rw-r--r--vernac/vernacexpr.ml9
22 files changed, 157 insertions, 215 deletions
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 <https://github.com/coq/coq/pull/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
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
diff --git a/stm/stm.ml b/stm/stm.ml
index 95c58b9043..109ac2d8b4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2569,28 +2569,32 @@ end (* }}} *)
(********************************* STM API ************************************)
(******************************************************************************)
-(* Main initialization routine *)
-type stm_init_options = {
- (* The STM will set some internal flags differently depending on the
- specified [doc_type]. This distinction should disappear at some
- some point. *)
- doc_type : stm_doc_type;
-
- (* Initial load path in scope for the document. Usually extracted
- from -R options / _CoqProject *)
- iload_path : Loadpath.coq_path list;
-
- (* Require [require_libs] before the initial state is
+(** STM initialization options: *)
+type stm_init_options =
+ { doc_type : stm_doc_type
+ (** The STM does set some internal flags differently depending on
+ the specified [doc_type]. This distinction should disappear at
+ some some point. *)
+
+ ; ml_load_path : CUnix.physical_path list
+ (** OCaml load paths for the document. *)
+
+ ; vo_load_path : Loadpath.vo_path list
+ (** [vo] load paths for the document. Usually extracted from -R
+ options / _CoqProject *)
+
+ ; require_libs : (string * string option * bool option) list
+ (** Require [require_libs] before the initial state is
ready. Parameters follow [Library], that is to say,
[lib,prefix,import_export] means require library [lib] from
optional [prefix] and [import_export] if [Some false/Some true]
is used. *)
- require_libs : (string * string option * bool option) list;
- (* STM options that apply to the current document. *)
- stm_options : AsyncOpts.stm_opt;
-}
-(* fb_handler : Feedback.feedback -> unit; *)
+ ; stm_options : AsyncOpts.stm_opt
+ (** Low-level STM options *)
+ }
+
+ (* fb_handler : Feedback.feedback -> unit; *)
(*
let doc_type_module_name (std : stm_doc_type) =
@@ -2615,7 +2619,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 +2637,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..e56bac6e0f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,38 +52,30 @@ type stm_doc_type =
| VioDoc of string (* file path *)
| Interactive of interactive_top (* module path *)
-(** Coq initialization options:
-
- - [doc_type]: Type of document being created.
-
- - [require_libs]: list of libraries/modules to be pre-loaded at
- startup. A tuple [(modname,modfrom,import)] is equivalent to [From
- modfrom Require modname]; [import] works similarly to
- [Library.require_library_from_dirpath], [Some false] will import
- the module, [Some true] will additionally export it.
-
-*)
-type stm_init_options = {
- (* The STM will set some internal flags differently depending on the
- specified [doc_type]. This distinction should disappear at some
- some point. *)
- doc_type : stm_doc_type;
-
- (* Initial load path in scope for the document. Usually extracted
- from -R options / _CoqProject *)
- iload_path : Loadpath.coq_path list;
-
- (* Require [require_libs] before the initial state is
+(** STM initialization options: *)
+type stm_init_options =
+ { doc_type : stm_doc_type
+ (** The STM does set some internal flags differently depending on
+ the specified [doc_type]. This distinction should disappear at
+ some some point. *)
+
+ ; ml_load_path : CUnix.physical_path list
+ (** OCaml load paths for the document. *)
+
+ ; vo_load_path : Loadpath.vo_path list
+ (** [vo] load paths for the document. Usually extracted from -R
+ options / _CoqProject *)
+
+ ; require_libs : (string * string option * bool option) list
+ (** Require [require_libs] before the initial state is
ready. Parameters follow [Library], that is to say,
[lib,prefix,import_export] means require library [lib] from
optional [prefix] and [import_export] if [Some false/Some true]
is used. *)
- require_libs : (string * string option * bool option) list;
- (* STM options that apply to the current document. *)
- stm_options : AsyncOpts.stm_opt;
-}
-(* fb_handler : Feedback.feedback -> unit; *)
+ ; stm_options : AsyncOpts.stm_opt
+ (** Low-level STM options *)
+ }
(** The type of a STM document *)
type doc
diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake
index aa68fad39e..38c610a5a6 100644
--- a/test-suite/ide/debug_ltac.fake
+++ b/test-suite/ide/debug_ltac.fake
@@ -1,2 +1,3 @@
+ADD { Comments "fakeide doesn't support fail as the first sentence". }
FAILADD { Debug On. }
ADD { Set Debug On. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index 5284c5d3a5..eb553f9dfa 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,6 +3,7 @@
#
# Simple backtrack by 2 before two global definitions
#
+ADD initial { Comments "initial sentence". }
ADD { Definition foo := 0. }
ADD { Definition bar := 1. }
EDIT_AT initial
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 }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 8486de3aed..37b584f8d9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -912,10 +912,11 @@ GRAMMAR EXTEND Gram
| IDENT "Locate"; l = locatable -> { VernacLocate l }
(* Managing load paths *)
- | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
- { VernacAddLoadPath (false, dir, alias) }
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
- alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
+ | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+ { VernacAddLoadPath { implicit = false; logical_path; physical_path } }
+ | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+ { VernacAddLoadPath { implicit = true; logical_path; physical_path } }
+
| IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
{ VernacRemoveLoadPath dir }
@@ -934,9 +935,7 @@ GRAMMAR EXTEND Gram
| IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) }
| IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (false, dir) }
- | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
- { VernacAddMLPath (true, dir) }
+ { VernacAddMLPath dir }
(* For acting on parameter tables *)
| "Set"; table = option_table; v = option_setting ->
@@ -1070,9 +1069,6 @@ GRAMMAR EXTEND Gram
option_table:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
;
- as_dirpath:
- [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ]
- ;
ne_in_or_out_modules:
[ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
| IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 506b3bc505..38aa42c349 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -218,24 +218,18 @@ let try_locate_absolute_library dir =
(** { 5 Extending the load path } *)
-(* Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
- unix_path : string; (* Filesystem path containing vo/ml files *)
- coq_path : DP.t; (* Coq prefix for the path *)
- implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
- has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
-}
-
-type coq_path_spec =
- | VoPath of vo_path_spec
- | MlPath of string
-
-type coq_path = {
- path_spec: coq_path_spec;
- recursive: bool;
-}
+type vo_path =
+ { unix_path : string
+ (** Filesystem path containing vo/ml files *)
+ ; coq_path : DP.t
+ (** Coq prefix for the path *)
+ ; implicit : bool
+ (** [implicit = true] avoids having to qualify with [coq_path] *)
+ ; has_ml : bool
+ (** If [has_ml] is true, the directory will also be added to the ml include path *)
+ ; recursive : bool
+ (** [recursive] will determine whether we explore sub-directories *)
+ }
let warn_cannot_open_path =
CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
@@ -255,9 +249,10 @@ let convert_string d =
warn_cannot_use_directory d;
raise Exit
-let add_vo_path ~recursive lp =
+let add_vo_path lp =
let unix_path = lp.unix_path in
let implicit = lp.implicit in
+ let recursive = lp.recursive in
if System.exists_dir unix_path then
let dirs = if recursive then System.all_subdirs ~unix_path else [] in
let prefix = DP.repr lp.coq_path in
@@ -268,22 +263,17 @@ let add_vo_path ~recursive lp =
with Exit -> None
in
let dirs = List.map_filter convert_dirs dirs in
- let add_ml_dir = Mltop.add_ml_dir ~recursive:false in
- let () = match lp.has_ml with
- | AddNoML -> ()
- | AddTopML ->
- Mltop.add_ml_dir ~recursive:false unix_path
- | AddRecML ->
- List.iter (fun (lp,_) -> add_ml_dir lp) dirs;
- add_ml_dir unix_path in
+ let () =
+ if lp.has_ml && not lp.recursive then
+ Mltop.add_ml_dir unix_path
+ else if lp.has_ml && lp.recursive then
+ (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs;
+ Mltop.add_ml_dir unix_path)
+ else
+ ()
+ in
let add (path, dir) = add_load_path path ~implicit dir in
let () = List.iter add dirs in
add_load_path unix_path ~implicit lp.coq_path
else
warn_cannot_open_path unix_path
-
-let add_coq_path { recursive; path_spec } = match path_spec with
- | VoPath lp ->
- add_vo_path ~recursive lp
- | MlPath dir ->
- Mltop.add_ml_dir ~recursive dir
diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index 47d2d34125..68212b9a47 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string
(** {6 Extending the Load Path } *)
(** Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
- unix_path : string;
+type vo_path =
+ { unix_path : string
(** Filesystem path containing vo/ml files *)
- coq_path : Names.DirPath.t;
+ ; coq_path : DirPath.t
(** Coq prefix for the path *)
- implicit : bool;
+ ; implicit : bool
(** [implicit = true] avoids having to qualify with [coq_path] *)
- has_ml : add_ml;
- (** If [has_ml] is true, the directory will also be search for plugins *)
-}
-
-type coq_path_spec =
- | VoPath of vo_path_spec
- | MlPath of string
-
-type coq_path = {
- path_spec: coq_path_spec;
- recursive: bool;
-}
+ ; has_ml : bool
+ (** If [has_ml] is true, the directory will also be added to the ml include path *)
+ ; recursive : bool
+ (** [recursive] will determine whether we explore sub-directories *)
+ }
-val add_coq_path : coq_path -> unit
+val add_vo_path : vo_path -> unit
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 5046248e11..671dae7876 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -128,11 +128,6 @@ let add_ml_dir s =
| WithoutTop when has_dynlink -> keep_copy_mlpath s
| _ -> ()
-(* For Rec Add ML Path (-R) *)
-let add_ml_dir ~recursive unix_path =
- let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in
- List.iter (fun (lp,_) -> add_ml_dir lp) dirs
-
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
if Filename.check_suffix name ".cmo" then
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 271772d7ba..633a5c241d 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit
(** {5 ML Dynlink} *)
(** Adds a dir to the plugin search path *)
-val add_ml_dir : recursive:bool -> string -> unit
+val add_ml_dir : string -> unit
(** Tests if we can load ML files *)
val has_dynlink : bool
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 314c423f65..33d9e3d98a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1016,22 +1016,18 @@ let string_of_definition_object_kind = let open Decls in function
return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
(* Auxiliary file and library management *)
- | VernacAddLoadPath (fl,s,d) ->
+ | VernacAddLoadPath { implicit; physical_path; logical_path } ->
return (
hov 2
(keyword "Add" ++
- (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
- keyword "LoadPath" ++ spc() ++ qs s ++
- (match d with
- | None -> mt()
- | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
- )
+ (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+ keyword "LoadPath" ++ spc() ++ qs physical_path ++
+ spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
| VernacRemoveLoadPath s ->
return (keyword "Remove LoadPath" ++ qs s)
- | VernacAddMLPath (fl,s) ->
+ | VernacAddMLPath (s) ->
return (
keyword "Add"
- ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
++ keyword "ML Path"
++ qs s
)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2eb1aa39b0..3cf4b4a89d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t =
let expand filename =
Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
-let vernac_add_loadpath implicit pdir ldiropt =
+let vernac_add_loadpath ~implicit pdir coq_path =
let open Loadpath in
let pdir = expand pdir in
- let alias = Option.default Libnames.default_root_prefix ldiropt in
- add_coq_path { recursive = true;
- path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
+ add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true }
let vernac_remove_loadpath path =
Loadpath.remove_load_path (expand path)
(* Coq syntax for ML or system commands *)
-let vernac_add_ml_path isrec path =
- let open Loadpath in
- add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
+let vernac_add_ml_path path =
+ Mltop.add_ml_dir (expand path)
let vernac_declare_ml_module ~local l =
let local = Option.default false local in
@@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
unsupported_attributes atts;
vernac_solve_existential ~pstate n c)
(* Auxiliary file and library management *)
- | VernacAddLoadPath (isrec,s,alias) ->
+ | VernacAddLoadPath { implicit; physical_path; logical_path } ->
VtDefault(fun () ->
unsupported_attributes atts;
- vernac_add_loadpath isrec s alias)
+ vernac_add_loadpath ~implicit physical_path logical_path)
| VernacRemoveLoadPath s ->
VtDefault(fun () ->
unsupported_attributes atts;
vernac_remove_loadpath s)
- | VernacAddMLPath (isrec,s) ->
+ | VernacAddMLPath (s) ->
VtDefault(fun () ->
unsupported_attributes atts;
- vernac_add_ml_path isrec s)
+ vernac_add_ml_path s)
| VernacDeclareMLModule l ->
VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
| VernacChdir s ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 45018a246c..22aaab2a68 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -98,7 +98,6 @@ type search_restriction =
| SearchInside of qualid list
| SearchOutside of qualid list
-type rec_flag = bool (* true = Rec; false = NoRec *)
type verbose_flag = bool (* true = Verbose; false = Silent *)
type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
type instance_flag = bool option
@@ -363,9 +362,13 @@ type nonrec vernac_expr =
| VernacSolveExistential of int * constr_expr
(* Auxiliary file and library management *)
- | VernacAddLoadPath of rec_flag * string * DirPath.t option
+ | VernacAddLoadPath of { implicit : bool
+ ; physical_path : CUnix.physical_path
+ ; logical_path : DirPath.t
+ }
+
| VernacRemoveLoadPath of string
- | VernacAddMLPath of rec_flag * string
+ | VernacAddMLPath of string
| VernacDeclareMLModule of string list
| VernacChdir of string option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:08:55 +0000