diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:44 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:44 +0000 |
commit | f5ab2e37b0609d8edb8d65dfae49741442a90657 (patch) | |
tree | 72bb704f147a824b743566b447c4e98685ab2db6 /checker/check.ml | |
parent | 5635c35ea4ec172fd81147effed4f33e2f581aaa (diff) |
Revised infrastructure for lazy loading of opaque proofs
Get rid of the LightenLibrary hack : no more last-minute
collect of opaque terms and Obj.magic tricks. Instead, we
make coqc accumulate the opaque terms as soon as constant_bodies
are created outside sections. In these cases, the opaque
terms are placed in a special table, and some (DirPath.t * int)
are used as indexes in constant_body. In an interactive session,
the local opaque terms stay directly stored in the constant_body.
The structure of .vo file stays similar : magic number, regular
library structure, digest of the first part, array of opaque terms.
In addition, we now have a final checksum for checking the
integrity of the whole .vo file. The other difference is that
lazy_constr aren't changed into int indexes in .vo files, but are
now coded as (substitution list * DirPath.t * int). In particular
this approach allows to refer to opaque terms from another
library. This (and accumulating substitutions in lazy_constr)
seems to greatly help decreasing the size of opaque tables :
-20% of vo size on the standard library :-). The compilation times
are slightly better, but that can be statistic noise.
The -force-load-proofs isn't active anymore : it behaves now
just like -lazy-load-proofs. The -dont-load-proofs mode has
slightly changed : opaque terms aren't seen as axioms anymore,
but accessing their bodies will raise an error.
Btw, API change : Declareops.body_of_constant now produces directly
a constr option instead of a constr_substituted option
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.ml')
-rw-r--r-- | checker/check.ml | 37 |
1 files changed, 30 insertions, 7 deletions
diff --git a/checker/check.ml b/checker/check.ml index eb4016f5f..1b9fd0701 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -40,7 +40,7 @@ type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; - md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library; + md_compiled : Safe_typing.compiled_library; md_objects : library_objects; md_deps : (compilation_unit_name * Digest.t) array; md_imports : compilation_unit_name array } @@ -56,6 +56,7 @@ type library_t = { library_name : compilation_unit_name; library_filename : CUnix.physical_path; library_compiled : Safe_typing.compiled_library; + library_opaques : Term.constr array; library_deps : (compilation_unit_name * Digest.t) array; library_digest : Digest.t } @@ -91,6 +92,19 @@ let library_full_filename dir = (find_library dir).library_filename let register_loaded_library m = libraries_table := LibraryMap.add m.library_name m !libraries_table +(* Map from library names to table of opaque terms *) +let opaque_tables = ref LibraryMap.empty + +let access_opaque_table dp i = + let t = + try LibraryMap.find dp !opaque_tables + with Not_found -> assert false + in + assert (i < Array.length t); + t.(i) + +let _ = Declarations.indirect_opaque_access := access_opaque_table + let check_one_lib admit (dir,m) = let file = m.library_filename in let md = m.library_compiled in @@ -105,7 +119,7 @@ let check_one_lib admit (dir,m) = else (Flags.if_verbose ppnl (str "Checking library: " ++ pr_dirpath dir); - Safe_typing.import file md dig); + Safe_typing.import file md m.library_opaques dig); Flags.if_verbose pp (fnl()); pp_flush (); register_loaded_library m @@ -280,7 +294,8 @@ let with_magic_number_check f a = let mk_library md f table digest = { library_name = md.md_name; library_filename = f; - library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled; + library_compiled = md.md_compiled; + library_opaques = table; library_deps = md.md_deps; library_digest = digest } @@ -298,16 +313,24 @@ let intern_from_file (dir, f) = try let ch = with_magic_number_check raw_intern_library f in let (md:library_disk) = System.marshal_in f ch in - let digest = System.marshal_in f ch in - let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in - close_in ch; + let (digest:Digest.t) = System.marshal_in f ch in + let (table:Term.constr array) = System.marshal_in f ch in + (* Verification of the final checksum *) + let pos = pos_in ch in + let (checksum:Digest.t) = System.marshal_in f ch in + let () = close_in ch in + let ch = open_in f in + if not (String.equal (Digest.channel ch pos) checksum) then + errorlabstrm "intern_from_file" (str "Checksum mismatch"); + let () = close_in ch in if dir <> md.md_name then - errorlabstrm "load_physical_library" + errorlabstrm "intern_from_file" (name_clash_message dir md.md_name f); Flags.if_verbose ppnl (str" done]"); md,table,digest with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; + opaque_tables := LibraryMap.add md.md_name table !opaque_tables; mk_library md f table digest let get_deps (dir, f) = |