From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Sep 2015 12:25:35 +0200 Subject: The -require option now accepts a logical path instead of a physical one. --- CHANGES | 2 ++ doc/refman/RefMan-com.tex | 6 +++--- library/library.ml | 20 +++++--------------- library/library.mli | 3 +-- man/coqide.1 | 10 +++++----- man/coqtop.1 | 8 ++++---- toplevel/coqtop.ml | 8 ++++---- toplevel/usage.ml | 2 +- toplevel/vernacentries.mli | 3 +++ 9 files changed, 28 insertions(+), 34 deletions(-) diff --git a/CHANGES b/CHANGES index e3224db04..950f2fab1 100644 --- a/CHANGES +++ b/CHANGES @@ -54,6 +54,8 @@ Tools - The -compile command-line option now takes the full path of the considered file, including the ".v" extension, and outputs a warning if such an extension is lacking. +- The -require command-line option now takes a logical path of a given library + rather than a physical path. Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 2f9758fde..0f1823a02 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -157,10 +157,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Load \Coq~compiled file {\em file}{\tt .vo} -\item[{\tt -require} {\em file}]\ +\item[{\tt -require} {\em path}]\ - Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt - Require} {\em file}). + Load \Coq~compiled library {\em path} and import it (equivalent to {\tt + Require Import} {\em path}). \item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ diff --git a/library/library.ml b/library/library.ml index 1bcffcd14..a09f91b15 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,18 +488,8 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let check_library_short_name f dir = function - | Some id when not (Id.equal id (snd (split_dirpath dir))) -> - errorlabstrm "check_library_short_name" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ - pr_id id) - | _ -> () - -let rec_intern_by_filename_only id f = +let rec_intern_by_filename_only f = let m = try intern_from_file f with Sys_error s -> error s in - (* Only the base name is expected to match *) - check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin @@ -518,12 +508,12 @@ let native_name_from_filename f = let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file idopt f = +let rec_intern_library_from_file f = (* A name is specified, we have to check it contains library id *) let paths = Loadpath.get_paths () in let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only idopt f + rec_intern_by_filename_only f (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a @@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file idopt file export = - let modref,needed = rec_intern_library_from_file idopt file in +let require_library_from_file file export = + let modref,needed = rec_intern_library_from_file file in let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); diff --git a/library/library.mli b/library/library.mli index f2e60718d..3d96f9a75 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,8 +22,7 @@ open Libnames (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit -val require_library_from_file : - Id.t option -> CUnix.physical_path -> bool option -> unit +val require_library_from_file : CUnix.physical_path -> bool option -> unit (** {6 Start the compilation of a library } *) diff --git a/man/coqide.1 b/man/coqide.1 index 3fa7f0e41..cfd9c3b4a 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -67,11 +67,11 @@ Load Coq file Load Coq object file .IR f .vo. .TP -.BI \-require\ f -Load Coq object file -.IR f .vo -and import it (Require -.IR f .). +.BI \-require\ path +Load Coq library +.IR path +and import it (Require Import +.IR path .). .TP .BI \-compile\ f Compile Coq file diff --git a/man/coqtop.1 b/man/coqtop.1 index 705ea43f6..e079bee39 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -78,10 +78,10 @@ load Coq object file .I filename.vo .TP -.BI \-require \ filename -load Coq object file -.I filename.vo -and import it (Require Import filename.) +.BI \-require \ path +load Coq library +.I path +and import it (Require Import path.) .TP .BI \-compile \ filename.v diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d67559d77..32ac9a496 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -171,7 +171,7 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter (fun f -> Library.require_library_from_file None f None) + List.iter (fun f -> Library.require_library_from_file f None) (List.rev !load_vernacular_obj) let require_prelude () = @@ -185,9 +185,9 @@ let require_prelude () = let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - if !load_init then silently require_prelude (); - List.iter (fun s -> Library.require_library_from_file None s (Some false)) - (List.rev !require_list) + let () = if !load_init then silently require_prelude () in + let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) let compile_list = ref ([] : (bool * string) list) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 3c001eadc..472503ced 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -42,7 +42,7 @@ let print_usage_channel co command = \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\ \n -lv f (idem)\ \n -load-vernac-object f load Coq object file f.vo\ -\n -require f load Coq object file f.vo and import it (Require f.)\ +\n -require path load Coq library path and import it (Require Import path.)\ \n -compile f.v compile Coq file f.v (implies -batch)\ \n -compile-verbose f.v verbosely compile Coq file f.v (implies -batch)\ \n -quick quickly compile .v files to .vio files (skip proofs)\ diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 4b1cd7a01..c6d87596d 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -16,6 +16,9 @@ val show_prooftree : unit -> unit val show_node : unit -> unit +val vernac_require : + Libnames.reference option -> bool option -> Libnames.reference list -> unit + (** This function can be used by any command that want to observe terms in the context of the current goal *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env -- cgit v1.2.3