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.

---
 vernac/library.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'vernac')

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.
---
 vernac/library.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'vernac')

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