diff options
| author | Emilio Jesus Gallego Arias | 2020-05-14 01:35:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-14 01:35:34 +0200 |
| commit | 2a43f3ef8e932f55a8f697ae24fef7075e62eb54 (patch) | |
| tree | befaf2a5c4a5df31f576226a2d5bb8e53761a090 /lib | |
| parent | 91b5990e724acc863a5dba66acc33fd698ac26f0 (diff) | |
| parent | 9e315837fded9763c3d7ca14a8aad0e7af3b4820 (diff) | |
Merge PR #12244: Store the OCaml version used for Coq in vo files.
Reviewed-by: ejgallego
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 9 | ||||
| -rw-r--r-- | lib/system.mli | 2 |
2 files changed, 11 insertions, 0 deletions
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 |