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. --- 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 ++--- 8 files changed, 54 insertions(+), 91 deletions(-) (limited to 'vernac') 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 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(-) (limited to 'vernac') 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