From bfe93b7c7b737ae2b1ccb52ffc05a5b241cc9c20 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 10 Jun 2019 23:06:45 +0200 Subject: [library] Move library to vernac This is step 1 on removing library state from the lower layers. Here we move library loading to the vernacular layer; few things depend on it: - printers: we add a parameter for those needing to access on-disk data, - coqlib: indeed a few tactics do try to check that a particular library is loaded; this is a tricky part. I've replaced that for a module name check, but indeed this is fully equivalent due to side-effects of `Require`. We may want to think what to do here. A few other minor code movements were needed, but there are self-explanatory. --- library/coqlib.ml | 6 +- library/library.ml | 642 ----------------------------------------------- library/library.mli | 77 ------ library/library.mllib | 1 - library/states.ml | 8 - library/states.mli | 3 - printing/prettyp.ml | 101 ++++---- printing/prettyp.mli | 47 ++-- toplevel/coqc.ml | 5 +- toplevel/coqtop.ml | 2 +- vernac/library.ml | 651 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/library.mli | 81 ++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 12 +- 14 files changed, 830 insertions(+), 807 deletions(-) delete mode 100644 library/library.ml delete mode 100644 library/library.mli create mode 100644 vernac/library.ml create mode 100644 vernac/library.mli diff --git a/library/coqlib.ml b/library/coqlib.ml index b1e4ef2b00..11d053624c 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -104,8 +104,10 @@ let gen_reference_in_modules locstr dirs s = let check_required_library d = let dir = make_dir d in - if Library.library_is_loaded dir then () - else + try + let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in + () + with Not_found -> let in_current_dir = match Lib.current_mp () with | MPfile dp -> DirPath.equal dir dp | _ -> false diff --git a/library/library.ml b/library/library.ml deleted file mode 100644 index 0faef7bf84..0000000000 --- a/library/library.ml +++ /dev/null @@ -1,642 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* in_channel -> 'a delayed * Digest.t -val fetch_delayed : 'a delayed -> 'a - -end = -struct - -type 'a delayed = { - del_file : string; - del_off : int; - del_digest : Digest.t; -} - -let in_delayed f ch = - let pos = pos_in ch in - let _, digest = System.skip_in_segment f ch in - ({ del_file = f; del_digest = digest; del_off = pos; }, digest) - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_delayed del = - let { del_digest = digest; del_file = f; del_off = pos; } = del in - try - let ch = raw_intern_library f in - let () = seek_in ch pos in - let obj, _, digest' = System.marshal_in_segment f ch in - let () = close_in ch in - if not (String.equal digest digest') then raise (Faulty f); - obj - with e when CErrors.noncritical e -> raise (Faulty f) - -end - -open Delayed - - -(************************************************************************) -(*s Modules on disk contain the following informations (after the magic - number, and before the digest). *) - -type compilation_unit_name = DirPath.t - -type library_disk = { - md_compiled : Safe_typing.compiled_library; - md_objects : Declaremods.library_objects; -} - -type summary_disk = { - md_name : compilation_unit_name; - md_imports : compilation_unit_name array; - md_deps : (compilation_unit_name * Safe_typing.vodigest) array; -} - -(*s Modules loaded in memory contain the following informations. They are - kept in the global table [libraries_table]. *) - -type library_t = { - library_name : compilation_unit_name; - library_data : library_disk delayed; - library_deps : (compilation_unit_name * Safe_typing.vodigest) array; - library_imports : compilation_unit_name array; - library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.ContextSet.t; -} - -type library_summary = { - libsum_name : compilation_unit_name; - libsum_digests : Safe_typing.vodigest; - libsum_imports : compilation_unit_name array; -} - -module LibraryOrdered = DirPath -module LibraryMap = Map.Make(LibraryOrdered) -module LibraryFilenameMap = Map.Make(LibraryOrdered) - -(* This is a map from names to loaded libraries *) -let libraries_table : library_summary LibraryMap.t ref = - Summary.ref LibraryMap.empty ~name:"LIBRARY" - -(* This is the map of loaded libraries filename *) -(* (not synchronized so as not to be caught in the states on disk) *) -let libraries_filename_table = ref LibraryFilenameMap.empty - -(* These are the _ordered_ sets of loaded, imported and exported libraries *) -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" - -(* various requests to the tables *) - -let find_library dir = - LibraryMap.find dir !libraries_table - -let try_find_library dir = - try find_library dir - with Not_found -> - 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 *) - (* from a previous play of the session *) - libraries_filename_table := - LibraryFilenameMap.add dir f !libraries_filename_table - -let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table - with Not_found -> "" - -let overwrite_library_filenames f = - let f = - if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in - LibraryMap.iter (fun dir _ -> register_library_filename dir f) - !libraries_table - -let library_is_loaded dir = - try let _ = find_library dir in true - with Not_found -> false - -let library_is_opened dir = - List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list - -let loaded_libraries () = !libraries_loaded_list - -let opened_libraries () = !libraries_imports_list - - (* If a library is loaded several time, then the first occurrence must - be performed first, thus the libraries_loaded_list ... *) - -let register_loaded_library m = - let libname = m.libsum_name in - let link () = - let dirname = Filename.dirname (library_full_filename libname) in - let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in - let f = prefix ^ "cmo" in - let f = Dynlink.adapt_filename f in - if Coq_config.native_compiler then - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f - in - let rec aux = function - | [] -> link (); [libname] - | m'::_ as l when DirPath.equal m' libname -> l - | m'::l' -> m' :: aux l' in - libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add libname m !libraries_table - - (* ... while if a library is imported/exported several time, then - only the last occurrence is really needed - though the imported - list may differ from the exported list (consider the sequence - Export A; Export B; Import A which results in A;B for exports but - in B;A for imports) *) - -let rec remember_last_of_each l m = - match l with - | [] -> [m] - | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m - | m'::l' -> m' :: remember_last_of_each l' m - -let register_open_library export m = - libraries_imports_list := remember_last_of_each !libraries_imports_list m; - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(************************************************************************) -(*s Opening libraries *) - -(* [open_library export explicit m] opens library [m] if not already - opened _or_ if explicitly asked to be (re)opened *) - -let open_library export explicit_libs m = - if - (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentioned by the user are always reopen *) - List.exists (fun m' -> DirPath.equal m m') explicit_libs - || not (library_is_opened m) - then begin - register_open_library export m; - Declaremods.really_import_module (MPfile m) - end - else - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(* open_libraries recursively open a list of libraries but opens only once - a library that is re-exported many times *) - -let open_libraries export modl = - let to_open_list = - List.fold_left - (fun l m -> - let subimport = - Array.fold_left - (fun l m -> remember_last_of_each l m) - l m.libsum_imports - in remember_last_of_each subimport m.libsum_name) - [] modl in - let explicit = List.map (fun m -> m.libsum_name) modl in - List.iter (open_library export explicit) to_open_list - - -(**********************************************************************) -(* import and export of libraries - synchronous operations *) -(* at the end similar to import and export of modules except that it *) -(* is optimized: when importing several libraries at the same time *) -(* which themselves indirectly imports the very same modules, these *) -(* ones are imported only ones *) - -let open_import_library i (_,(modl,export)) = - if Int.equal i 1 then - (* even if the library is already imported, we re-import it *) - (* if not (library_is_opened dir) then *) - open_libraries export (List.map try_find_library modl) - -let cache_import_library obj = - open_import_library 1 obj - -let subst_import_library (_,o) = o - -let classify_import_library (_,export as obj) = - if export then Substitute obj else Dispose - -let in_import_library : DirPath.t list * bool -> obj = - declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import_library; - open_function = open_import_library; - subst_function = subst_import_library; - classify_function = classify_import_library } - -(************************************************************************) -(** {6 Tables of opaque proof terms} *) - -(** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, - we can quickly load a first half of a .vo file without these opaque - terms, and access them only when a specific command (e.g. Print or - Print Assumptions) needs it. *) - -(** Delayed / available tables of opaque terms *) - -type 'a table_status = - | ToFetch of 'a array delayed - | Fetched of 'a array - -let opaque_tables = - ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) - -let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_tables - -let access_table what tables dp i = - let t = match LibraryMap.find dp !tables with - | Fetched t -> t - | ToFetch f -> - let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let t = - try fetch_delayed f - with Faulty f -> - 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") - in - tables := LibraryMap.add dp (Fetched t) !tables; - t - in - assert (i < Array.length t); t.(i) - -let access_opaque_table dp i = - let what = "opaque proofs" in - access_table what opaque_tables dp i - -let indirect_accessor = { - Opaqueproof.access_proof = access_opaque_table; - Opaqueproof.access_discharge = Cooking.cook_constr; -} - -(************************************************************************) -(* Internalise libraries *) - -type seg_sum = summary_disk -type seg_lib = library_disk -type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm array - -let mk_library sd md digests univs = - { - library_name = sd.md_name; - library_data = md; - library_deps = sd.md_deps; - library_imports = sd.md_imports; - library_digests = digests; - library_extra_univs = univs; - } - -let mk_summary m = { - libsum_name = m.library_name; - libsum_imports = m.library_imports; - libsum_digests = m.library_digests; -} - -let intern_from_file f = - let ch = raw_intern_library f in - let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in - let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in - let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in - let _ = System.skip_in_segment f ch in - let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in - close_in ch; - register_library_filename lsd.md_name f; - add_opaque_table lsd.md_name (ToFetch del_opaque); - let open Safe_typing in - match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - | Some (uall,true) -> - mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (_,false) -> - mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - -module DPMap = Map.Make(DirPath) - -let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = - (* Look if in the current logical environment *) - try (find_library dir).libsum_digests, (needed, contents) - with Not_found -> - (* Look if already listed and consequently its dependencies too *) - try (DPMap.find dir contents).library_digests, (needed, contents) - with Not_found -> - Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); - (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> lib_resolver dir in - let m = intern_from_file f in - if not (DirPath.equal dir m.library_name) then - user_err ~hdr:"load_physical_library" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - 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 ~lib_resolver (needed, contents) dir m f - -and intern_library_deps ~lib_resolver libs dir m from = - let needed, contents = - Array.fold_left (intern_mandatory_library ~lib_resolver dir from) - libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) - -and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = - let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in - if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err (str "Compiled library " ++ DirPath.print caller ++ - str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ - over library " ++ DirPath.print dir); - libs - -let rec_intern_library ~lib_resolver libs (dir, f) = - let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in - libs - -let native_name_from_filename f = - let ch = 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 - -(**********************************************************************) -(*s [require_library] loads and possibly opens a library. This is a - synchronized operation. It is performed as follows: - - preparation phase: (functions require_library* ) the library and its - dependencies are read from to disk (using intern_* ) - [they are read from disk to ensure that at section/module - discharging time, the physical library referred to outside the - section/module is the one that was used at type-checking time in - the section/module] - - execution phase: (through add_leaf and cache_require) - the library is loaded in the environment and Nametab, the objects are - registered etc, using functions from Declaremods (via load_library, - which recursively loads its dependencies) -*) - -let register_library m = - let l = fetch_delayed m.library_data in - Declaremods.register_library - m.library_name - l.md_compiled - l.md_objects - m.library_digests - m.library_extra_univs; - register_loaded_library (mk_summary m) - -(* Follow the semantics of Anticipate object: - - called at module or module type closing when a Require occurs in - the module or module type - - not called from a library (i.e. a module identified with a file) *) -let load_require _ (_,(needed,modl,_)) = - List.iter register_library needed - -let open_require i (_,(_,modl,export)) = - Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) - export - - (* [needed] is the ordered list of libraries not already loaded *) -let cache_require o = - load_require 1 o; - open_require 1 o - -let discharge_require (_,o) = Some o - -(* open_function is never called from here because an Anticipate object *) - -type require_obj = library_t list * DirPath.t list * bool option - -let in_require : require_obj -> obj = - declare_object {(default_object "REQUIRE") with - cache_function = cache_require; - load_function = load_require; - open_function = (fun _ _ -> assert false); - discharge_function = discharge_require; - classify_function = (fun o -> Anticipate o) } - -(* Require libraries, import them if [export <> None], mark them for export - if [export = Some true] *) - -let warn_require_in_module = - CWarnings.create ~name:"require-in-module" ~category:"deprecated" - (fun () -> strbrk "Require inside a module is" ++ - strbrk " deprecated and strongly discouraged. " ++ - strbrk "You can Require a module at toplevel " ++ - strbrk "and optionally Import it inside another one.") - -let require_library_from_dirpath ~lib_resolver modrefl export = - let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in - let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in - let modrefl = List.map fst modrefl in - if Lib.is_module_or_modtype () then - begin - warn_require_in_module (); - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - add_anonymous_leaf (in_import_library (modrefl,exp))) - export - end - else - add_anonymous_leaf (in_require (needed,modrefl,export)); - () - -(* the function called by Vernacentries.vernac_import *) - -let safe_locate_module qid = - try Nametab.locate_module qid - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module" - (pr_qualid qid ++ str " is not a module") - -let import_module export modl = - (* Optimization: libraries in a raw in the list are imported - "globally". If there is non-library in the list; it breaks the - optimization For instance: "Import Arith MyModule Zarith" will - not be optimized (possibly resulting in redefinitions, but - "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" - will have the submodules imported by both Arith and ZArith - imported only once *) - let flush = function - | [] -> () - | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in - let rec aux acc = function - | qid :: l -> - let m,acc = - try Nametab.locate_module qid, acc - with Not_found-> flush acc; safe_locate_module qid, [] in - (match m with - | MPfile dir -> aux (dir::acc) l - | mp -> - flush acc; - try Declaremods.import_module export mp; aux [] l - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_module" - (pr_qualid qid ++ str " is not a module")) - | [] -> flush acc - in aux [] modl - -(************************************************************************) -(*s Initializing the compilation of a library. *) - -let load_library_todo f = - let ch = raw_intern_library f in - let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in - let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in - let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let tasks, _, _ = System.marshal_in_segment f ch in - let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in - close_in ch; - 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 snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get tasks, s4 - -(************************************************************************) -(*s [save_library dir] ends library [dir] and save it to the disk. *) - -let current_deps () = - let map name = - let m = try_find_library name in - (name, m.libsum_digests) - in - List.map map !libraries_loaded_list - -let current_reexports () = !libraries_exports_list - -let error_recursively_dependent_library 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.") - -(* We now use two different digests in a .vo file. The first one - only covers half of the file, without the opaque table. It is - used for identifying this version of this library : this digest - is the one leading to "inconsistent assumptions" messages. - The other digest comes at the very end, and covers everything - before it. This one is used for integrity check of the whole - file when loading the opaque table. *) - -(* Security weakness: file might have been changed on disk between - writing the content and computing the checksum... *) - -let save_library_to ?todo ~output_native_objects dir f otab = - let except = match todo with - | None -> - (* XXX *) - (* assert(!Flags.compilation_mode = Flags.BuildVo); *) - assert(Filename.check_suffix f ".vo"); - Future.UUIDSet.empty - | Some (l,_) -> - assert(Filename.check_suffix f ".vio"); - List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) - Future.UUIDSet.empty l in - let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab = - match todo with - | None -> None, None - | Some (tasks, rcbackup) -> - let tasks = - List.map Stateid.(fun (r,b) -> - try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b - with Not_found -> assert b; { r with uuid = -1 }, b) - tasks in - Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false) - in - let sd = { - md_name = dir; - md_deps = Array.of_list (current_deps ()); - md_imports = Array.of_list (current_reexports ()); - } in - let md = { - md_compiled = cenv; - md_objects = seg; - } in - if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then - error_recursively_dependent_library dir; - (* Open the vo file and write the magic number *) - let f' = f in - let ch = raw_extern_library f' in - try - (* Writing vo payload *) - System.marshal_out_segment f' ch (sd : seg_sum); - System.marshal_out_segment f' ch (md : seg_lib); - System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (tasks : 'tasks option); - System.marshal_out_segment f' ch (opaque_table : seg_proofs); - close_out ch; - (* Writing native code files *) - if output_native_objects then - let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - Nativelib.compile_library dir ast fn - with reraise -> - let reraise = CErrors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in - let () = close_out ch in - let () = Sys.remove f' in - iraise reraise - -let save_library_raw f sum lib univs proofs = - let ch = raw_extern_library f in - System.marshal_out_segment f ch (sum : seg_sum); - System.marshal_out_segment f ch (lib : seg_lib); - System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : 'tasks option); - System.marshal_out_segment f ch (proofs : seg_proofs); - close_out ch - -module StringOrd = struct type t = string let compare = String.compare end -module StringSet = Set.Make(StringOrd) - -let get_used_load_paths () = - StringSet.elements - (List.fold_left (fun acc m -> StringSet.add - (Filename.dirname (library_full_filename m)) acc) - StringSet.empty !libraries_loaded_list) - -let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/library.mli b/library/library.mli deleted file mode 100644 index bb6c42e393..0000000000 --- a/library/library.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* CUnix.physical_path) - -> (DirPath.t * string) list - -> bool option - -> unit - -(** {6 Start the compilation of a library } *) - -(** Segments of a library *) -type seg_sum -type seg_lib -type seg_univ = (* all_cst, finished? *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm array - -(** Open a module (or a library); if the boolean is true then it's also - an export otherwise just a simple import *) -val import_module : bool -> qualid list -> unit - -(** End the compilation of a library and save it to a ".vo" file. - [output_native_objects]: when producing vo objects, also compile the native-code version. *) -val save_library_to : - ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> - output_native_objects:bool -> - DirPath.t -> string -> Opaqueproof.opaquetab -> unit - -val load_library_todo - : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs - -val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit - -(** {6 Interrogate the status of libraries } *) - - (** - Tell if a library is loaded or opened *) -val library_is_loaded : DirPath.t -> bool -val library_is_opened : DirPath.t -> bool - - (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> DirPath.t list -val opened_libraries : unit -> DirPath.t list - - (** - Return the full filename of a loaded library. *) -val library_full_filename : DirPath.t -> string - - (** - Overwrite the filename of all libraries (used when restoring a state) *) -val overwrite_library_filenames : string -> unit - -(** {6 Native compiler. } *) -val native_name_from_filename : string -> string - -(** {6 Opaque accessors} *) -val indirect_accessor : Opaqueproof.indirect_accessor diff --git a/library/library.mllib b/library/library.mllib index 3b75438ccd..c34d8911e8 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -6,7 +6,6 @@ Nametab Global Lib Declaremods -Library States Kindops Goptions diff --git a/library/states.ml b/library/states.ml index a73f16957d..0be153d96a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -9,7 +9,6 @@ (************************************************************************) open Util -open System type state = Lib.frozen * Summary.frozen @@ -25,13 +24,6 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let extern_state s = - System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) - -let intern_state s = - unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); - Library.overwrite_library_filenames s - (* Rollback. *) let with_state_protection f x = diff --git a/library/states.mli b/library/states.mli index c4f3eae49d..4870f48fc3 100644 --- a/library/states.mli +++ b/library/states.mli @@ -15,9 +15,6 @@ freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) -val intern_state : string -> unit -val extern_state : string -> unit - type state val freeze : marshallable:bool -> state val unfreeze : state -> unit diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f82b9cef68..4f1300f178 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,14 +35,14 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -552,10 +552,10 @@ let print_instance sigma cb = let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() - -let print_constant with_values sep sp udecl = + +let print_constant indirect_accessor with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in + let val_0 = Global.body_of_constant_body indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -563,7 +563,7 @@ let print_constant with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -593,8 +593,8 @@ let print_constant with_values sep sp udecl = (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos sp udecl = - print_constant true " = " sp udecl ++ +let gallina_print_constant_with_infos indirect_accessor sp udecl = + print_constant indirect_accessor true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -610,7 +610,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -621,7 +621,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant with_values sep (Constant.make1 kn) None) + Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| @@ -637,24 +637,24 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = Some (print_modtype (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry env sigma with_values ent = +let gallina_print_library_entry indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry env sigma with_values (oname,lobj) + gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> - Some (str " >>>>>>> Section " ++ pr_name oname) + Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> - Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> - Some (str " >>>>>>> Module " ++ pr_name oname) + Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context env sigma with_values = +let gallina_print_context indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry env sigma with_values h with - | None -> prec n rest - | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + (match gallina_print_library_entry indirect_accessor env sigma with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec @@ -712,10 +712,10 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) -let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) +let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context env sigma = +let print_full_pure_context ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -731,8 +731,8 @@ let print_full_pure_context env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)) - | Def c -> + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ pr_lconstr_env env sigma (Mod_subst.force_constr c) @@ -779,11 +779,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context env sigma sec = - print_context env sigma true None (read_sec_context sec) +let print_sec_context indirect_accessor env sigma sec = + print_context indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ env sigma sec = - print_context env sigma false None (read_sec_context sec) +let print_sec_context_typ indirect_accessor env sigma sec = + print_context indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -793,11 +793,11 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name env sigma na udecl = +let print_any_name indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos sp udecl + | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp @@ -816,34 +816,34 @@ let print_any_name env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name env sigma na udecl = +let print_name indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + print_any_name indirect_accessor env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) - udecl + udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name env sigma (locate_any_name ref) udecl + print_any_name indirect_accessor env sigma (locate_any_name ref) udecl -let print_opaque_name env sigma qid = +let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then - print_constant_with_infos cst None - else - user_err Pp.(str "Not a defined constant.") + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then + print_constant_with_infos indirect_accessor cst None + else + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> - print_inductive sp None + print_inductive sp None | ConstructRef cstr as gr -> - let ty, ctx = Typeops.type_of_global_in_context env gr in - let ty = EConstr.of_constr ty in - let open EConstr in - print_typed_value_in_env env sigma (mkConstruct cstr, ty) + let ty, ctx = Typeops.type_of_global_in_context env gr in + let ty = EConstr.of_constr ty in + let open EConstr in + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> print_named_decl env sigma + env |> lookup_named id |> print_named_decl env sigma let print_about_any ?loc env sigma k udecl = maybe_error_reject_univ_decl k udecl; @@ -880,9 +880,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect env sigma depth = - print_context env sigma false (Some depth) (Lib.contents ()) - +let inspect indirect_accessor env sigma depth = + print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 7485f4bd19..4299bcc880 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -18,22 +18,41 @@ open Libnames val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context : env -> Evd.evar_map -> Pp.t -val print_full_context_typ : env -> Evd.evar_map -> Pp.t -val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t +val print_context + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t +val print_full_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + +val print_full_pure_context + : library_accessor:Opaqueproof.indirect_accessor + -> env + -> Evd.evar_map + -> Pp.t + +val print_sec_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_name + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option -> Pp.t +val print_opaque_name + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -50,7 +69,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : env -> Evd.evar_map -> int -> Pp.t +val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -83,14 +102,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 019577ac85..7658ad68a5 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -11,7 +11,7 @@ let outputstate opts = Option.iter (fun ostate_file -> let fname = CUnix.make_suffix ostate_file ".coq" in - States.extern_state fname) opts.Coqcargs.outputstate + Library.extern_state fname) opts.Coqcargs.outputstate let coqc_init _copts ~opts = Flags.quiet := true; @@ -53,7 +53,8 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + let library_accessor = Library.indirect_accessor in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f09d202edf..33a95e7b30 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -87,7 +87,7 @@ let set_options = List.iter set_option let inputstate opts = Option.iter (fun istate_file -> let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in - States.intern_state fname) opts.inputstate + Library.intern_state fname) opts.inputstate (******************************************************************************) (* Fatal Errors *) diff --git a/vernac/library.ml b/vernac/library.ml new file mode 100644 index 0000000000..e91cb965f5 --- /dev/null +++ b/vernac/library.ml @@ -0,0 +1,651 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* in_channel -> 'a delayed * Digest.t +val fetch_delayed : 'a delayed -> 'a + +end = +struct + +type 'a delayed = { + del_file : string; + del_off : int; + del_digest : Digest.t; +} + +let in_delayed f ch = + let pos = pos_in ch in + let _, digest = System.skip_in_segment f ch in + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) + +let fetch_delayed del = + let { del_digest = digest; del_file = f; del_off = pos; } = del in + try + let ch = raw_intern_library f in + let () = seek_in ch pos in + let obj, _, digest' = System.marshal_in_segment f ch in + let () = close_in ch in + if not (String.equal digest digest') then raise (Faulty f); + obj + with e when CErrors.noncritical e -> raise (Faulty f) + +end + +open Delayed + + +(************************************************************************) +(*s Modules on disk contain the following informations (after the magic + number, and before the digest). *) + +type compilation_unit_name = DirPath.t + +type library_disk = { + md_compiled : Safe_typing.compiled_library; + md_objects : Declaremods.library_objects; +} + +type summary_disk = { + md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : (compilation_unit_name * Safe_typing.vodigest) array; +} + +(*s Modules loaded in memory contain the following informations. They are + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_data : library_disk delayed; + library_deps : (compilation_unit_name * Safe_typing.vodigest) array; + library_imports : compilation_unit_name array; + library_digests : Safe_typing.vodigest; + library_extra_univs : Univ.ContextSet.t; +} + +type library_summary = { + libsum_name : compilation_unit_name; + libsum_digests : Safe_typing.vodigest; + libsum_imports : compilation_unit_name array; +} + +module LibraryOrdered = DirPath +module LibraryMap = Map.Make(LibraryOrdered) +module LibraryFilenameMap = Map.Make(LibraryOrdered) + +(* This is a map from names to loaded libraries *) +let libraries_table : library_summary LibraryMap.t ref = + Summary.ref LibraryMap.empty ~name:"LIBRARY" + +(* This is the map of loaded libraries filename *) +(* (not synchronized so as not to be caught in the states on disk) *) +let libraries_filename_table = ref LibraryFilenameMap.empty + +(* These are the _ordered_ sets of loaded, imported and exported libraries *) +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" + +(* various requests to the tables *) + +let find_library dir = + LibraryMap.find dir !libraries_table + +let try_find_library dir = + try find_library dir + with Not_found -> + 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 *) + (* from a previous play of the session *) + libraries_filename_table := + LibraryFilenameMap.add dir f !libraries_filename_table + +let library_full_filename dir = + try LibraryFilenameMap.find dir !libraries_filename_table + with Not_found -> "" + +let overwrite_library_filenames f = + let f = + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in + LibraryMap.iter (fun dir _ -> register_library_filename dir f) + !libraries_table + +let library_is_loaded dir = + try let _ = find_library dir in true + with Not_found -> false + +let library_is_opened dir = + List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list + +let loaded_libraries () = !libraries_loaded_list + +let opened_libraries () = !libraries_imports_list + + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) + +let register_loaded_library m = + let libname = m.libsum_name in + let link () = + let dirname = Filename.dirname (library_full_filename libname) in + let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in + let f = prefix ^ "cmo" in + let f = Dynlink.adapt_filename f in + if Coq_config.native_compiler then + Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f + in + let rec aux = function + | [] -> link (); [libname] + | m'::_ as l when DirPath.equal m' libname -> l + | m'::l' -> m' :: aux l' in + libraries_loaded_list := aux !libraries_loaded_list; + libraries_table := LibraryMap.add libname m !libraries_table + + (* ... while if a library is imported/exported several time, then + only the last occurrence is really needed - though the imported + list may differ from the exported list (consider the sequence + Export A; Export B; Import A which results in A;B for exports but + in B;A for imports) *) + +let rec remember_last_of_each l m = + match l with + | [] -> [m] + | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m + | m'::l' -> m' :: remember_last_of_each l' m + +let register_open_library export m = + libraries_imports_list := remember_last_of_each !libraries_imports_list m; + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +(************************************************************************) +(*s Opening libraries *) + +(* [open_library export explicit m] opens library [m] if not already + opened _or_ if explicitly asked to be (re)opened *) + +let open_library export explicit_libs m = + if + (* Only libraries indirectly to open are not reopen *) + (* Libraries explicitly mentioned by the user are always reopen *) + List.exists (fun m' -> DirPath.equal m m') explicit_libs + || not (library_is_opened m) + then begin + register_open_library export m; + Declaremods.really_import_module (MPfile m) + end + else + if export then + libraries_exports_list := remember_last_of_each !libraries_exports_list m + +(* open_libraries recursively open a list of libraries but opens only once + a library that is re-exported many times *) + +let open_libraries export modl = + let to_open_list = + List.fold_left + (fun l m -> + let subimport = + Array.fold_left + (fun l m -> remember_last_of_each l m) + l m.libsum_imports + in remember_last_of_each subimport m.libsum_name) + [] modl in + let explicit = List.map (fun m -> m.libsum_name) modl in + List.iter (open_library export explicit) to_open_list + + +(**********************************************************************) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) + +let open_import_library i (_,(modl,export)) = + if Int.equal i 1 then + (* even if the library is already imported, we re-import it *) + (* if not (library_is_opened dir) then *) + open_libraries export (List.map try_find_library modl) + +let cache_import_library obj = + open_import_library 1 obj + +let subst_import_library (_,o) = o + +let classify_import_library (_,export as obj) = + if export then Substitute obj else Dispose + +let in_import_library : DirPath.t list * bool -> obj = + declare_object {(default_object "IMPORT LIBRARY") with + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } + +(************************************************************************) +(** {6 Tables of opaque proof terms} *) + +(** We now store opaque proof terms apart from the rest of the environment. + See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, + we can quickly load a first half of a .vo file without these opaque + terms, and access them only when a specific command (e.g. Print or + Print Assumptions) needs it. *) + +(** Delayed / available tables of opaque terms *) + +type 'a table_status = + | ToFetch of 'a array delayed + | Fetched of 'a array + +let opaque_tables = + ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) + +let add_opaque_table dp st = + opaque_tables := LibraryMap.add dp st !opaque_tables + +let access_table what tables dp i = + let t = match LibraryMap.find dp !tables with + | Fetched t -> t + | ToFetch f -> + let dir_path = Names.DirPath.to_string dp in + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let t = + try fetch_delayed f + with Faulty f -> + 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") + in + tables := LibraryMap.add dp (Fetched t) !tables; + t + in + assert (i < Array.length t); t.(i) + +let access_opaque_table dp i = + let what = "opaque proofs" in + access_table what opaque_tables dp i + +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = Cooking.cook_constr; +} + +(************************************************************************) +(* Internalise libraries *) + +type seg_sum = summary_disk +type seg_lib = library_disk +type seg_univ = (* true = vivo, false = vi *) + Univ.ContextSet.t * bool +type seg_proofs = Opaqueproof.opaque_proofterm array + +let mk_library sd md digests univs = + { + library_name = sd.md_name; + library_data = md; + library_deps = sd.md_deps; + library_imports = sd.md_imports; + library_digests = digests; + library_extra_univs = univs; + } + +let mk_summary m = { + libsum_name = m.library_name; + libsum_imports = m.library_imports; + libsum_digests = m.library_digests; +} + +let intern_from_file f = + let ch = raw_intern_library f in + let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in + let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in + let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in + let _ = System.skip_in_segment f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in + close_in ch; + register_library_filename lsd.md_name f; + add_opaque_table lsd.md_name (ToFetch del_opaque); + let open Safe_typing in + match univs with + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + | Some (uall,true) -> + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall + | Some (_,false) -> + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + +module DPMap = Map.Make(DirPath) + +let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = + (* Look if in the current logical environment *) + try (find_library dir).libsum_digests, (needed, contents) + with Not_found -> + (* Look if already listed and consequently its dependencies too *) + try (DPMap.find dir contents).library_digests, (needed, contents) + with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); + (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let f = match f with Some f -> f | None -> lib_resolver dir in + let m = intern_from_file f in + if not (DirPath.equal dir m.library_name) then + user_err ~hdr:"load_physical_library" + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ + 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 ~lib_resolver (needed, contents) dir m f + +and intern_library_deps ~lib_resolver libs dir m from = + let needed, contents = + Array.fold_left (intern_mandatory_library ~lib_resolver dir from) + libs m.library_deps in + (dir :: needed, DPMap.add dir m contents ) + +and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = + let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in + if not (Safe_typing.digest_match ~actual:digest ~required:d) then + user_err (str "Compiled library " ++ DirPath.print caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ DirPath.print dir); + libs + +let rec_intern_library ~lib_resolver libs (dir, f) = + let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in + libs + +let native_name_from_filename f = + let ch = 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 + +(**********************************************************************) +(*s [require_library] loads and possibly opens a library. This is a + synchronized operation. It is performed as follows: + + preparation phase: (functions require_library* ) the library and its + dependencies are read from to disk (using intern_* ) + [they are read from disk to ensure that at section/module + discharging time, the physical library referred to outside the + section/module is the one that was used at type-checking time in + the section/module] + + execution phase: (through add_leaf and cache_require) + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, + which recursively loads its dependencies) +*) + +let register_library m = + let l = fetch_delayed m.library_data in + Declaremods.register_library + m.library_name + l.md_compiled + l.md_objects + m.library_digests + m.library_extra_univs; + register_loaded_library (mk_summary m) + +(* Follow the semantics of Anticipate object: + - called at module or module type closing when a Require occurs in + the module or module type + - not called from a library (i.e. a module identified with a file) *) +let load_require _ (_,(needed,modl,_)) = + List.iter register_library needed + +let open_require i (_,(_,modl,export)) = + Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) + export + + (* [needed] is the ordered list of libraries not already loaded *) +let cache_require o = + load_require 1 o; + open_require 1 o + +let discharge_require (_,o) = Some o + +(* open_function is never called from here because an Anticipate object *) + +type require_obj = library_t list * DirPath.t list * bool option + +let in_require : require_obj -> obj = + declare_object {(default_object "REQUIRE") with + cache_function = cache_require; + load_function = load_require; + open_function = (fun _ _ -> assert false); + discharge_function = discharge_require; + classify_function = (fun o -> Anticipate o) } + +(* Require libraries, import them if [export <> None], mark them for export + if [export = Some true] *) + +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + +let require_library_from_dirpath ~lib_resolver modrefl export = + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in + let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in + let modrefl = List.map fst modrefl in + if Lib.is_module_or_modtype () then + begin + warn_require_in_module (); + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun exp -> + add_anonymous_leaf (in_import_library (modrefl,exp))) + export + end + else + add_anonymous_leaf (in_require (needed,modrefl,export)); + () + +(* the function called by Vernacentries.vernac_import *) + +let safe_locate_module qid = + try Nametab.locate_module qid + with Not_found -> + user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module" + (pr_qualid qid ++ str " is not a module") + +let import_module export modl = + (* Optimization: libraries in a raw in the list are imported + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | qid :: l -> + let m,acc = + try Nametab.locate_module qid, acc + with Not_found-> flush acc; safe_locate_module qid, [] in + (match m with + | MPfile dir -> aux (dir::acc) l + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err ?loc:qid.CAst.loc ~hdr:"import_module" + (pr_qualid qid ++ str " is not a module")) + | [] -> flush acc + in aux [] modl + +(************************************************************************) +(*s Initializing the compilation of a library. *) + +let load_library_todo f = + let ch = raw_intern_library f in + let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in + let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in + let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in + let tasks, _, _ = System.marshal_in_segment f ch in + let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in + close_in ch; + 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 snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); + s0, s1, Option.get s2, Option.get tasks, s4 + +(************************************************************************) +(*s [save_library dir] ends library [dir] and save it to the disk. *) + +let current_deps () = + let map name = + let m = try_find_library name in + (name, m.libsum_digests) + in + List.map map !libraries_loaded_list + +let current_reexports () = !libraries_exports_list + +let error_recursively_dependent_library 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.") + +(* We now use two different digests in a .vo file. The first one + only covers half of the file, without the opaque table. It is + used for identifying this version of this library : this digest + is the one leading to "inconsistent assumptions" messages. + The other digest comes at the very end, and covers everything + before it. This one is used for integrity check of the whole + file when loading the opaque table. *) + +(* Security weakness: file might have been changed on disk between + writing the content and computing the checksum... *) + +let save_library_to ?todo ~output_native_objects dir f otab = + let except = match todo with + | None -> + (* XXX *) + (* assert(!Flags.compilation_mode = Flags.BuildVo); *) + assert(Filename.check_suffix f ".vo"); + Future.UUIDSet.empty + | Some (l,_) -> + assert(Filename.check_suffix f ".vio"); + List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) + Future.UUIDSet.empty l in + let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in + let opaque_table, f2t_map = Opaqueproof.dump ~except otab in + let tasks, utab = + match todo with + | None -> None, None + | Some (tasks, rcbackup) -> + let tasks = + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in + Some (tasks,rcbackup), + Some (Univ.ContextSet.empty,false) + in + let sd = { + md_name = dir; + md_deps = Array.of_list (current_deps ()); + md_imports = Array.of_list (current_reexports ()); + } in + let md = { + md_compiled = cenv; + md_objects = seg; + } in + if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then + error_recursively_dependent_library dir; + (* Open the vo file and write the magic number *) + let f' = f in + let ch = raw_extern_library f' in + try + (* Writing vo payload *) + System.marshal_out_segment f' ch (sd : seg_sum); + System.marshal_out_segment f' ch (md : seg_lib); + System.marshal_out_segment f' ch (utab : seg_univ option); + System.marshal_out_segment f' ch (tasks : 'tasks option); + System.marshal_out_segment f' ch (opaque_table : seg_proofs); + close_out ch; + (* Writing native code files *) + if output_native_objects then + let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in + Nativelib.compile_library dir ast fn + with reraise -> + let reraise = CErrors.push reraise in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in + let () = close_out ch in + let () = Sys.remove f' in + iraise reraise + +let save_library_raw f sum lib univs proofs = + let ch = raw_extern_library f in + System.marshal_out_segment f ch (sum : seg_sum); + System.marshal_out_segment f ch (lib : seg_lib); + System.marshal_out_segment f ch (Some univs : seg_univ option); + System.marshal_out_segment f ch (None : 'tasks option); + System.marshal_out_segment f ch (proofs : seg_proofs); + close_out ch + +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) + +let get_used_load_paths () = + StringSet.elements + (List.fold_left (fun acc m -> StringSet.add + (Filename.dirname (library_full_filename m)) acc) + StringSet.empty !libraries_loaded_list) + +let _ = Nativelib.get_load_paths := get_used_load_paths + +(* These commands may not be very safe due to ML-side plugin loading + etc... use at your own risk *) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true) + +let intern_state s = + States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + overwrite_library_filenames s diff --git a/vernac/library.mli b/vernac/library.mli new file mode 100644 index 0000000000..973b369226 --- /dev/null +++ b/vernac/library.mli @@ -0,0 +1,81 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* CUnix.physical_path) + -> (DirPath.t * string) list + -> bool option + -> unit + +(** {6 Start the compilation of a library } *) + +(** Segments of a library *) +type seg_sum +type seg_lib +type seg_univ = (* all_cst, finished? *) + Univ.ContextSet.t * bool +type seg_proofs = Opaqueproof.opaque_proofterm array + +(** Open a module (or a library); if the boolean is true then it's also + an export otherwise just a simple import *) +val import_module : bool -> qualid list -> unit + +(** End the compilation of a library and save it to a ".vo" file. + [output_native_objects]: when producing vo objects, also compile the native-code version. *) +val save_library_to : + ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + output_native_objects:bool -> + DirPath.t -> string -> Opaqueproof.opaquetab -> unit + +val load_library_todo + : CUnix.physical_path + -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs + +val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit + +(** {6 Interrogate the status of libraries } *) + + (** - Tell if a library is loaded or opened *) +val library_is_loaded : DirPath.t -> bool +val library_is_opened : DirPath.t -> bool + + (** - Tell which libraries are loaded or imported *) +val loaded_libraries : unit -> DirPath.t list +val opened_libraries : unit -> DirPath.t list + + (** - Return the full filename of a loaded library. *) +val library_full_filename : DirPath.t -> string + + (** - Overwrite the filename of all libraries (used when restoring a state) *) +val overwrite_library_filenames : string -> unit + +(** {6 Native compiler. } *) +val native_name_from_filename : string -> string + +(** {6 Opaque accessors} *) +val indirect_accessor : Opaqueproof.indirect_accessor + +(** Low-level state overwriting, not very safe *) +val intern_state : string -> unit +val extern_state : string -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 20de6b4ff2..cd13f83e96 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -16,6 +16,7 @@ DeclareDef DeclareObl Canonical RecLemmas +Library Lemmas Class Auto_ind_decl diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4ae9d6d54f..80a1700ac7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1161,11 +1161,11 @@ let vernac_chdir = function let vernac_write_state file = let file = CUnix.make_suffix file ".coq" in - States.extern_state file + Library.extern_state file let vernac_restore_state file = let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in - States.intern_state file + Library.intern_state file (************) (* Commands *) @@ -1954,9 +1954,9 @@ let vernac_print ~pstate ~atts = function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ env sigma - | PrintSectionContext qid -> print_sec_context_typ env sigma qid - | PrintInspect n -> inspect env sigma n + | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir @@ -1969,7 +1969,7 @@ let vernac_print ~pstate ~atts = | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name env sigma qid udecl + print_name Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() -- cgit v1.2.3