From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Sep 2015 11:04:59 +0200 Subject: Make -load-vernac-object respect the loadpath. This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq. --- CHANGES | 5 +++-- doc/refman/RefMan-com.tex | 4 ++-- library/library.ml | 34 ---------------------------------- library/library.mli | 1 - man/coqide.1 | 8 +++++--- man/coqtop.1 | 7 ++++--- toplevel/coqtop.ml | 4 ++-- 7 files changed, 16 insertions(+), 47 deletions(-) diff --git a/CHANGES b/CHANGES index 950f2fab1..16d86c8ff 100644 --- a/CHANGES +++ b/CHANGES @@ -54,8 +54,9 @@ 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. +- The -require and -load-vernac-object command-line options now take a logical + path of a given library rather than a physical path, thus they behave like + Require [Import] path. Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 0f1823a02..9862abb53 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the standard input. -\item[{\tt -load-vernac-object} {\em file}]\ +\item[{\tt -load-vernac-object} {\em path}]\ - Load \Coq~compiled file {\em file}{\tt .vo} + Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}). \item[{\tt -require} {\em path}]\ diff --git a/library/library.ml b/library/library.ml index a09f91b15..6d7b0f603 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,33 +488,11 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let rec_intern_by_filename_only f = - let m = try intern_from_file f with Sys_error s -> error s in - (* We check no other file containing same library is loaded *) - if library_is_loaded m.library_name then - begin - msg_warning - (pr_dirpath m.library_name ++ str " is already loaded from file " ++ - str (library_full_filename m.library_name)); - m.library_name, [] - end - else - let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in - let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in - m.library_name, needed - let native_name_from_filename f = let ch = System.with_magic_number_check raw_intern_library f in 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 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 f - (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: @@ -590,18 +568,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -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)); - Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); - add_frozen_state () - (* the function called by Vernacentries.vernac_import *) let safe_locate_module (loc,qid) = diff --git a/library/library.mli b/library/library.mli index 3d96f9a75..d5e610dd6 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,6 @@ 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 : CUnix.physical_path -> bool option -> unit (** {6 Start the compilation of a library } *) diff --git a/man/coqide.1 b/man/coqide.1 index cfd9c3b4a..6a3e67ad5 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -63,9 +63,11 @@ Load Coq file (Load Verbose .IR f .). .TP -.BI \-load\-vernac\-object\ f -Load Coq object file -.IR f .vo. +.BI \-load\-vernac\-object\ path +Load Coq library +.IR path +(Require +.IR path .). .TP .BI \-require\ path Load Coq library diff --git a/man/coqtop.1 b/man/coqtop.1 index e079bee39..62d17aa67 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -73,9 +73,10 @@ load verbosely Coq file (Load Verbose filename.) .TP -.BI \-load\-vernac\-object \ filename -load Coq object file -.I filename.vo +.BI \-load\-vernac\-object \ path +load Coq library +.I path +(Require path.) .TP .BI \-require \ path diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 32ac9a496..b7f1e4a19 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -171,8 +171,8 @@ 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 f None) - (List.rev !load_vernacular_obj) + let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) let require_prelude () = let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in -- cgit v1.2.3