From 3e04d6c024dd03878b0b487cf823f5586d6fd397 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 3 May 2020 20:34:41 +0200 Subject: Store the OCaml version used for Coq in vo files. --- checker/check.ml | 9 +++++++++ checker/values.ml | 2 +- vernac/library.ml | 12 ++++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/checker/check.ml b/checker/check.ml index 31bfebc3d5..26de2db109 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -263,6 +263,7 @@ let raw_intern_library f = type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } module Dyn = Dyn.Make () @@ -289,6 +290,11 @@ let name_clash_message dir mdir f = pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir +let caml_version_mismatch s f = + str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++ + str s ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++ + spc() ++ str Coq_config.caml_version + type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *) (* Dependency graph *) @@ -345,6 +351,9 @@ let intern_from_file ~intern_mode (dir, f) = let () = close_in ch in let ch = open_in_bin f in let () = close_in ch in + if Coq_config.caml_version <> sd.md_ocaml then + user_err ~hdr:"intern_from_file" + (caml_version_mismatch sd.md_ocaml f); if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); diff --git a/checker/values.ml b/checker/values.ml index 76e3ab0d45..cce0ce7203 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) let v_libsum = - Tuple ("summary", [|v_dp;v_deps|]) + Tuple ("summary", [|v_dp;v_deps;String|]) let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) diff --git a/vernac/library.ml b/vernac/library.ml index 85db501e84..2cd642c7e8 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -89,6 +89,7 @@ type library_disk = { type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } (*s Modules loaded in memory contain the following informations. They are @@ -244,6 +245,14 @@ let mk_summary m = { libsum_digests = m.library_digests; } +let check_ocaml_version num f = + if not (String.equal num Coq_config.caml_version) then + user_err Pp.( + str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++ + str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++ + spc () ++ str Coq_config.caml_version + ) + let intern_from_file f = let ch = raw_intern_library f in let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in @@ -251,6 +260,7 @@ let intern_from_file f = let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; + check_ocaml_version lsd.md_ocaml f; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in @@ -401,6 +411,7 @@ let load_library_todo f = let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in ObjFile.close_in ch; + check_ocaml_version s0.md_ocaml f; 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"); @@ -486,6 +497,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); + md_ocaml = Coq_config.caml_version; } in let md = { md_compiled = cenv; -- cgit v1.2.3 From 9e315837fded9763c3d7ca14a8aad0e7af3b4820 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2020 12:55:19 +0200 Subject: Centralize the OCaml version-checking function. We tweak the message a bit. --- checker/check.ml | 9 +-------- lib/system.ml | 9 +++++++++ lib/system.mli | 2 ++ vernac/library.ml | 12 ++---------- 4 files changed, 14 insertions(+), 18 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 26de2db109..6d307b3c5e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -290,11 +290,6 @@ let name_clash_message dir mdir f = pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir -let caml_version_mismatch s f = - str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++ - str s ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++ - spc() ++ str Coq_config.caml_version - type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *) (* Dependency graph *) @@ -351,9 +346,7 @@ let intern_from_file ~intern_mode (dir, f) = let () = close_in ch in let ch = open_in_bin f in let () = close_in ch in - if Coq_config.caml_version <> sd.md_ocaml then - user_err ~hdr:"intern_from_file" - (caml_version_mismatch sd.md_ocaml f); + let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); diff --git a/lib/system.ml b/lib/system.ml index 4e98651d6e..e25f758865 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -168,6 +168,15 @@ let try_remove filename = let error_corrupted file s = CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") +let check_caml_version ~caml:s ~file:f = + if not (String.equal Coq_config.caml_version s) then + CErrors.user_err (str ("The file " ^ f ^ " was compiled with OCaml") ++ + spc () ++ str s ++ spc () ++ str "while this instance of Coq was compiled \ + with OCaml" ++ spc() ++ str Coq_config.caml_version ++ str "." ++ spc () ++ + str "Coq object files need to be compiled with the same OCaml toolchain to \ + be compatible.") + else () + let input_binary_int f ch = try input_binary_int ch with diff --git a/lib/system.mli b/lib/system.mli index 4a8c35b6ea..1e2f519327 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -88,6 +88,8 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val marshal_out : out_channel -> 'a -> unit val marshal_in : string -> in_channel -> 'a +val check_caml_version : caml:string -> file:string -> unit + (** {6 Time stamps.} *) type time diff --git a/vernac/library.ml b/vernac/library.ml index 2cd642c7e8..c30331b221 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -245,14 +245,6 @@ let mk_summary m = { libsum_digests = m.library_digests; } -let check_ocaml_version num f = - if not (String.equal num Coq_config.caml_version) then - user_err Pp.( - str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++ - str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++ - spc () ++ str Coq_config.caml_version - ) - let intern_from_file f = let ch = raw_intern_library f in let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in @@ -260,7 +252,7 @@ let intern_from_file f = let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; - check_ocaml_version lsd.md_ocaml f; + System.check_caml_version ~caml:lsd.md_ocaml ~file:f; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in @@ -411,7 +403,7 @@ let load_library_todo f = let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in ObjFile.close_in ch; - check_ocaml_version s0.md_ocaml f; + System.check_caml_version ~caml:s0.md_ocaml ~file:f; 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"); -- cgit v1.2.3