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 ------- ide/coq_commands.ml | 1 - ide/fake_ide.ml | 6 +-- stm/stm.ml | 8 ++-- stm/stm.mli | 3 +- test-suite/ide/debug_ltac.fake | 1 + test-suite/ide/undo002.fake | 1 + toplevel/ccompile.ml | 15 +++--- toplevel/coqargs.ml | 17 +++---- toplevel/coqargs.mli | 6 +-- toplevel/coqinit.ml | 51 ++++++++------------ toplevel/coqinit.mli | 4 +- toplevel/coqtop.ml | 6 +-- vernac/g_vernac.mlg | 15 ++---- vernac/loadpath.ml | 56 +++++++++------------- vernac/loadpath.mli | 29 ++++------- vernac/mltop.ml | 5 -- vernac/mltop.mli | 2 +- vernac/ppvernac.ml | 14 ++---- vernac/vernacentries.ml | 19 ++++---- vernac/vernacexpr.ml | 5 +- 22 files changed, 116 insertions(+), 173 deletions(-) create mode 100644 doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst 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 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..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, 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..df85e004ed 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -912,10 +912,10 @@ 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"; dir = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath (false, dir, logical_path) } + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath (true, dir, logical_path) } | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } @@ -934,9 +934,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 +1068,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..f58e9e7131 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 (fl,s,dir) -> 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 fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs s ++ + spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) | 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..e5cbb42fa6 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,s,coq_path) -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_loadpath isrec s alias) + vernac_add_loadpath ~implicit s coq_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..7feb05fe34 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,9 @@ type nonrec vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacAddLoadPath of bool * string * DirPath.t | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string + | VernacAddMLPath of string | VernacDeclareMLModule of string list | VernacChdir of string option -- cgit v1.2.3 From 8de81cf2b6059e1e5aa84ea483dba38e42b35792 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 20 Feb 2020 11:52:24 -0500 Subject: [stm] Port documentation of init options to ocamldoc --- stm/stm.ml | 39 +++++++++++++++++++++------------------ stm/stm.mli | 47 +++++++++++++++++++---------------------------- 2 files changed, 40 insertions(+), 46 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 6312bff5f3..109ac2d8b4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2569,29 +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 *) - ml_load_path : CUnix.physical_path list; - vo_load_path : Loadpath.vo_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) = diff --git a/stm/stm.mli b/stm/stm.mli index e242225cf2..e56bac6e0f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,39 +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 *) - ml_load_path : CUnix.physical_path list; - vo_load_path : Loadpath.vo_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 -- cgit v1.2.3 From 15ed46fffc962159ca6158aa791b5258fd42ab3c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 20 Feb 2020 13:06:22 -0500 Subject: [vernac] Use a record for VernacAddLoadPath --- vernac/g_vernac.mlg | 9 +++++---- vernac/ppvernac.ml | 8 ++++---- vernac/vernacentries.ml | 4 ++-- vernac/vernacexpr.ml | 6 +++++- 4 files changed, 16 insertions(+), 11 deletions(-) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index df85e004ed..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; "as"; logical_path = dirpath -> - { VernacAddLoadPath (false, dir, logical_path) } - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; "as"; logical_path = dirpath -> - { VernacAddLoadPath (true, dir, logical_path) } + | 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 } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f58e9e7131..33d9e3d98a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1016,13 +1016,13 @@ 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,dir) -> + | 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 ++ - 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 (s) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e5cbb42fa6..3cf4b4a89d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2103,10 +2103,10 @@ 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 (implicit,s,coq_path) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_loadpath ~implicit s coq_path) + vernac_add_loadpath ~implicit physical_path logical_path) | VernacRemoveLoadPath s -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 7feb05fe34..22aaab2a68 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -362,7 +362,11 @@ type nonrec vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacAddLoadPath of bool * string * DirPath.t + | VernacAddLoadPath of { implicit : bool + ; physical_path : CUnix.physical_path + ; logical_path : DirPath.t + } + | VernacRemoveLoadPath of string | VernacAddMLPath of string | VernacDeclareMLModule of string list -- cgit v1.2.3