From f43d96aec71449e3b75e9fd732e87694cec5db8f Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 21 Mar 2013 14:22:36 +0000 Subject: Removing mandatory suffixes for library files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/check.ml | 2 +- lib/system.ml | 13 ++++++------- lib/system.mli | 4 ++-- library/library.ml | 6 +++--- library/states.ml | 5 ++++- 5 files changed, 16 insertions(+), 14 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 88306e214..03a18280a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -264,7 +264,7 @@ let try_locate_qualified_library qid = (*s Loading from disk to cache (preparation phase) *) let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo") + snd (System.raw_extern_intern Coq_config.vo_magic_number) let with_magic_number_check f a = try f a diff --git a/lib/system.ml b/lib/system.ml index a72958b99..d2788de93 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -123,12 +123,11 @@ let marshal_in filename ch = exception Bad_magic_number of string -let raw_extern_intern magic suffix = - let extern_state name = - let filename = CUnix.make_suffix name suffix in +let raw_extern_intern magic = + let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename,channel + filename, channel and intern_state filename = let channel = open_in_bin filename in if not (Int.equal (input_binary_int channel) magic) then @@ -137,8 +136,8 @@ let raw_extern_intern magic suffix = in (extern_state,intern_state) -let extern_intern ?(warn=true) magic suffix = - let (raw_extern,raw_intern) = raw_extern_intern magic suffix in +let extern_intern ?(warn=true) magic = + let (raw_extern,raw_intern) = raw_extern_intern magic in let extern_state name val_0 = try let (filename,channel) = raw_extern name in @@ -152,7 +151,7 @@ let extern_intern ?(warn=true) magic suffix = with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,filename = find_file_in_path ~warn paths (CUnix.make_suffix name suffix) in + let _,filename = find_file_in_path ~warn paths name in let channel = raw_intern filename in let v = marshal_in filename channel in close_in channel; diff --git a/lib/system.mli b/lib/system.mli index 8cbbb9cab..c9c1df08a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,10 +36,10 @@ val marshal_in : string -> in_channel -> 'a exception Bad_magic_number of string -val raw_extern_intern : int -> string -> +val raw_extern_intern : int -> (string -> string * out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> string -> +val extern_intern : ?warn:bool -> int -> (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/library/library.ml b/library/library.ml index a5f93c02c..edb86bc4c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -318,7 +318,7 @@ let in_import : DirPath.t * bool -> obj = (*s Loading from disk to cache (preparation phase) *) let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number ".vo" + System.raw_extern_intern Coq_config.vo_magic_number (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -401,10 +401,10 @@ let mk_library md table 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; + let () = seek_in ch pos in if not (String.equal (System.marshal_in f ch) digest) then failwith "File changed!"; let table = (System.marshal_in f ch : LightenLibrary.table) in - close_in ch; + let () = close_in ch in table with e when Errors.noncritical e -> error diff --git a/library/states.ml b/library/states.ml index f30633171..906ebdacc 100644 --- a/library/states.ml +++ b/library/states.ml @@ -18,13 +18,16 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let (extern_state,intern_state) = + let ensure_suffix f = CUnix.make_suffix f ".coq" in let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number ".coq" in + extern_intern Coq_config.state_magic_number in (fun s -> + let s = ensure_suffix s in if !Flags.load_proofs <> Flags.Force then Errors.error "Write State only works with option -force-load-proofs"; raw_extern s (freeze())), (fun s -> + let s = ensure_suffix s in unfreeze (with_magic_number_check (raw_intern (Library.get_load_paths ())) s); Library.overwrite_library_filenames s) -- cgit v1.2.3