diff options
| -rw-r--r-- | checker/check.ml | 18 | ||||
| -rw-r--r-- | lib/system.ml | 71 | ||||
| -rw-r--r-- | lib/system.mli | 10 | ||||
| -rw-r--r-- | library/library.ml | 16 | ||||
| -rw-r--r-- | library/states.ml | 14 |
5 files changed, 58 insertions, 71 deletions
diff --git a/checker/check.ml b/checker/check.ml index c835cec82..2bc470aea 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -271,20 +271,10 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) +(*s Low-level interning of libraries from files *) -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) - -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) @@ -312,7 +302,7 @@ let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in + let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in diff --git a/lib/system.ml b/lib/system.ml index 139effd9f..ddc56956c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -174,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int filename channel) magic) then + raise (Bad_magic_number filename); channel - and intern_state filename = - try - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s -let extern_intern magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state filename val_0 = - try - let channel = raw_extern filename in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state filename = +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a diff --git a/lib/system.mli b/lib/system.mli index 5797502e9..247d528b9 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/library/library.ml b/library/library.ml index 0fb938e9b..6da9ccf68 100644 --- a/library/library.ml +++ b/library/library.ml @@ -19,10 +19,12 @@ open Lib (************************************************************************) (*s Low-level interning/externing of libraries to files *) -(*s Loading from disk to cache (preparation phase) *) +let raw_extern_library f = + System.raw_extern_state Coq_config.vo_magic_number f -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number +let raw_intern_library f = + System.with_magic_number_check + (System.raw_intern_state Coq_config.vo_magic_number) f (************************************************************************) (** Serialized objects loaded on-the-fly *) @@ -56,7 +58,7 @@ let in_delayed f ch = let fetch_delayed del = let { del_digest = digest; del_file = f; del_off = pos; } = del in try - let ch = System.with_magic_number_check raw_intern_library f in + 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 @@ -434,7 +436,7 @@ let mk_summary m = { } let intern_from_file f = - let ch = System.with_magic_number_check raw_intern_library f in + 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) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in @@ -489,7 +491,7 @@ let rec_intern_library libs mref = libs let native_name_from_filename f = - let ch = System.with_magic_number_check raw_intern_library f in + 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 @@ -654,7 +656,7 @@ let start_library f = let load_library_todo f = let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in - let ch = System.with_magic_number_check raw_intern_library f in + 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 diff --git a/library/states.ml b/library/states.ml index 4e55f0cdc..3cb6da12e 100644 --- a/library/states.ml +++ b/library/states.ml @@ -21,14 +21,12 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let (extern_state,intern_state) = - let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number in - (fun s -> - raw_extern s (freeze ~marshallable:`Yes)), - (fun s -> - unfreeze (with_magic_number_check raw_intern s); - Library.overwrite_library_filenames s) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes) + +let intern_state s = + unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s (* Rollback. *) |