summaryrefslogtreecommitdiff
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /library/library.ml
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml111
1 files changed, 45 insertions, 66 deletions
diff --git a/library/library.ml b/library/library.ml
index d44f796a..56d2709d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
@@ -12,9 +14,8 @@ open Util
open Names
open Libnames
-open Nameops
-open Libobject
open Lib
+open Libobject
(************************************************************************)
(*s Low-level interning/externing of libraries to files *)
@@ -97,7 +98,7 @@ type library_t = {
library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
library_imports : compilation_unit_name array;
library_digests : Safe_typing.vodigest;
- library_extra_univs : Univ.universe_context_set;
+ library_extra_univs : Univ.ContextSet.t;
}
type library_summary = {
@@ -131,8 +132,8 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- errorlabstrm "Library.find_library"
- (str "Unknown library " ++ pr_dirpath dir)
+ user_err ~hdr:"Library.find_library"
+ (str "Unknown library " ++ DirPath.print dir)
let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
@@ -171,7 +172,7 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- if not Coq_config.no_native_compiler then
+ if Coq_config.native_compiler then
Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
@@ -329,12 +330,12 @@ let locate_qualified_library ?root ?(warn = true) qid =
let error_unmapped_dir qid =
let prefix, _ = repr_qualid qid in
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
- str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+ str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ())
let error_lib_not_found qid =
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
let try_locate_absolute_library dir =
@@ -360,9 +361,9 @@ type 'a table_status =
| Fetched of 'a Future.computation array
let opaque_tables =
- ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+ ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
let univ_tables =
- ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t)
+ ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -378,7 +379,7 @@ let access_table what tables dp i =
let t =
try fetch_delayed f
with Faulty f ->
- errorlabstrm "Library.access_table"
+ user_err ~hdr:"Library.access_table"
(str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
str ") is inaccessible or corrupted,\ncannot load some " ++
str what ++ str " in it.\n")
@@ -408,9 +409,9 @@ let () =
type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
- Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
+ Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Term.constr Future.computation array
+type seg_proofs = Constr.constr Future.computation array
let mk_library sd md digests univs =
{
@@ -463,10 +464,10 @@ let rec intern_library (needed, contents) (dir, f) from =
let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
- errorlabstrm "load_physical_library"
+ user_err ~hdr:"load_physical_library"
(str "The file " ++ str f ++ str " contains library" ++ spc () ++
- pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
- spc() ++ pr_dirpath dir);
+ DirPath.print m.library_name ++ spc () ++ str "and not library" ++
+ spc() ++ DirPath.print dir);
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
m.library_digests, intern_library_deps (needed, contents) dir m f
@@ -477,9 +478,9 @@ and intern_library_deps libs dir m from =
and intern_mandatory_library caller from libs (dir,d) =
let digest, libs = intern_library libs (dir, None) (Some from) in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+ user_err (str "Compiled library " ++ DirPath.print caller ++
str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
- over library " ++ pr_dirpath dir);
+ over library " ++ DirPath.print dir);
libs
let rec_intern_library libs (dir, f) =
@@ -551,8 +552,6 @@ let in_require : require_obj -> obj =
(* Require libraries, import them if [export <> None], mark them for export
if [export = Some true] *)
-let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
-
let warn_require_in_module =
CWarnings.create ~name:"require-in-module" ~category:"deprecated"
(fun () -> strbrk "Require inside a module is" ++
@@ -574,16 +573,15 @@ let require_library_from_dirpath modrefl export =
end
else
add_anonymous_leaf (in_require (needed,modrefl,export));
- if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
- add_frozen_state ()
+ ()
(* the function called by Vernacentries.vernac_import *)
-let safe_locate_module (loc,qid) =
+let safe_locate_module {CAst.loc;v=qid} =
try Nametab.locate_module qid
with Not_found ->
- user_err_loc
- (loc,"import_library", pr_qualid qid ++ str " is not a module")
+ user_err ?loc ~hdr:"import_library"
+ (pr_qualid qid ++ str " is not a module")
let import_module export modl =
(* Optimization: libraries in a raw in the list are imported
@@ -597,7 +595,7 @@ let import_module export modl =
| [] -> ()
| modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
let rec aux acc = function
- | (loc,dir as m) :: l ->
+ | ({CAst.loc; v=dir} as m) :: l ->
let m,acc =
try Nametab.locate_module dir, acc
with Not_found-> flush acc; safe_locate_module m, [] in
@@ -607,8 +605,8 @@ let import_module export modl =
flush acc;
try Declaremods.import_module export mp; aux [] l
with Not_found ->
- user_err_loc (loc,"import_library",
- pr_qualid dir ++ str " is not a module"))
+ user_err ?loc ~hdr:"import_library"
+ (pr_qualid dir ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
@@ -619,39 +617,19 @@ let check_coq_overwriting p id =
let l = DirPath.repr p in
let is_empty = match l with [] -> true | _ -> false in
if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
- errorlabstrm ""
- (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+ user_err
+ (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
-(* Verifies that a string starts by a letter and do not contain
- others caracters than letters, digits, or `_` *)
-
-let check_module_name s =
- let msg c =
- strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++
- (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
- strbrk " is not allowed in module names\n"
- in
- let err c = errorlabstrm "" (msg c) in
- match String.get s 0 with
- | 'a' .. 'z' | 'A' .. 'Z' ->
- for i = 1 to (String.length s)-1 do
- match String.get s i with
- | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> ()
- | c -> err c
- done
- | c -> err c
-
let start_library fo =
let ldir0 =
try
let lp = Loadpath.find_load_path (Filename.dirname fo) in
Loadpath.logical lp
- with Not_found -> Nameops.default_root_prefix
+ with Not_found -> Libnames.default_root_prefix
in
let file = Filename.chop_extension (Filename.basename fo) in
let id = Id.of_string file in
- check_module_name file;
check_coq_overwriting ldir0 id;
let ldir = add_dirpath_suffix ldir0 id in
Declaremods.start_library ldir;
@@ -668,10 +646,10 @@ let load_library_todo f =
let tasks, _, _ = System.marshal_in_segment f ch in
let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
close_in ch;
- if tasks = None then errorlabstrm "restart" (str"not a .vio file");
- if s2 = None then errorlabstrm "restart" (str"not a .vio file");
- if s3 = None then errorlabstrm "restart" (str"not a .vio file");
- if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
+ if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
(************************************************************************)
@@ -687,8 +665,8 @@ let current_deps () =
let current_reexports () = !libraries_exports_list
let error_recursively_dependent_library dir =
- errorlabstrm ""
- (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
+ user_err
+ (strbrk "Unable to use logical name " ++ DirPath.print dir ++
strbrk " to save current library because" ++
strbrk " it already depends on a library of this name.")
@@ -706,7 +684,8 @@ let error_recursively_dependent_library dir =
let save_library_to ?todo dir f otab =
let except = match todo with
| None ->
- assert(!Flags.compilation_mode = Flags.BuildVo);
+ (* XXX *)
+ (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
assert(Filename.check_suffix f ".vo");
Future.UUIDSet.empty
| Some (l,_) ->
@@ -734,7 +713,7 @@ let save_library_to ?todo dir f otab =
except Int.Set.empty in
let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
Array.iteri (fun i x ->
- if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
+ if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
opaque_table;
let sd = {
@@ -761,10 +740,10 @@ let save_library_to ?todo dir f otab =
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
- if !Flags.native_compiler then
+ if !Flags.output_native_objects then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
- error "Could not compile the library to native code."
+ user_err Pp.(str "Could not compile the library to native code.")
with reraise ->
let reraise = CErrors.push reraise in
let () = Feedback.msg_warning (str "Removed file " ++ str f') in