diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/library.ml | 26 | ||||
| -rw-r--r-- | library/states.ml | 5 |
3 files changed, 25 insertions, 8 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index fad81b152..3f60bf96a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -157,7 +157,7 @@ let is_flexible_reference env bound depth f = | Rel n -> (* since local definitions have been expanded *) false | Const kn -> let cb = Environ.lookup_constant kn env in - cb.const_body <> None & not cb.const_opaque + (match cb.const_body with Def _ -> true | _ -> false) | Var id -> let (_,value,_) = Environ.lookup_named id env in value <> None | Ind _ | Construct _ -> false diff --git a/library/library.ml b/library/library.ml index 3d72c5fdb..447d53610 100644 --- a/library/library.ml +++ b/library/library.ml @@ -382,25 +382,39 @@ let try_locate_qualified_library (loc,qid) = (************************************************************************) (* Internalise libraries *) -let mk_library md get_table digest = - let md_compiled = - LightenLibrary.load ~load_proof:!Flags.load_proofs get_table md.md_compiled +let mk_library md table digest = + let md_compiled = + LightenLibrary.load ~load_proof:!Flags.load_proofs table md.md_compiled in { library_name = md.md_name; library_compiled = md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; library_imports = md.md_imports; - library_digest = digest + library_digest = digest } +let fetch_opaque_table (f,pos,digest) = + try + let ch = System.with_magic_number_check raw_intern_library f in + seek_in ch pos; + if System.marshal_in ch <> digest then failwith "File changed!"; + let table = (System.marshal_in ch : LightenLibrary.table) in + close_in ch; + table + with _ -> + error + ("The file "^f^" is inaccessible or has changed,\n" ^ + "cannot load some opaque constant bodies in it.\n") + let intern_from_file f = let ch = System.with_magic_number_check raw_intern_library f in let lmd = System.marshal_in ch in + let pos = pos_in ch in let digest = System.marshal_in ch in - let get_table () = (System.marshal_in ch : LightenLibrary.table) in + let table = lazy (fetch_opaque_table (f,pos,digest)) in register_library_filename lmd.md_name f; - let library = mk_library lmd get_table digest in + let library = mk_library lmd table digest in close_in ch; library diff --git a/library/states.ml b/library/states.ml index 4619b3b53..c88858f7e 100644 --- a/library/states.ml +++ b/library/states.ml @@ -20,7 +20,10 @@ let unfreeze (fl,fs) = let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number ".coq" in - (fun s -> raw_extern s (freeze())), + (fun s -> + if !Flags.load_proofs <> Flags.Force then + Util.error "Write State only works with option -force-load-proofs"; + raw_extern s (freeze())), (fun s -> unfreeze (with_magic_number_check (raw_intern (Library.get_load_paths ())) s); |