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 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'checker')

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|])
-- 
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 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'checker')

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);
-- 
cgit v1.2.3