diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 111 |
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 |