[configure] Allow to avoid embedding the date on Coq's binaries

This is quite important in some contexts, for example when using a
global compilation cache (as we do in Dune).

config/coq_config.mli

@@ -33,8 +33,8 @@ val arch_is_win32 : bool
 val version : string    (* version number of Coq *)
 val caml_version : string    (* OCaml version used to compile Coq *)
 val caml_version_nums : int list    (* OCaml version used to compile Coq by components *)
-val date : string       (* release date *)
-val compile_date : string (* compile date *)
+val date : string option         (* release date / None when in dev mode as to improve binary caching *)
+val compile_date : string option (* compile date / None when in dev mode as to improve binary caching *)
 val vo_version : int32
 val state_magic_number : int
 

config/dune

@@ -22,4 +22,4 @@
    ; Needed to generate include lists for coq_makefile
    plugin_list
   (env_var COQ_CONFIGURE_PREFIX))
- (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no -bin-annot))))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no -bin-annot -embed-date no))))

configure.ml

@@ -259,6 +259,7 @@ type preferences = {
   force_caml_version : bool;
   force_findlib_version : bool;
   warn_error : bool;
+  embed_date : bool;
 }
 
 module Profiles = struct
@@ -296,15 +297,17 @@ let default = {
   force_caml_version = false;
   force_findlib_version = false;
   warn_error = false;
+  embed_date = true;
 }
 
 let devel state = { state with
   local = true;
   bin_annot = true;
   annot = true;
   warn_error = true;
+  embed_date = false;
 }
-let devel_doc = "-local -annot -bin-annot -warn-error yes"
+let devel_doc = "-local -annot -bin-annot -warn-error yes -embed-date no"
 
 let get = function
   | "devel" -> devel
@@ -434,7 +437,10 @@ let args_options = Arg.align [
   "-camldir", Arg.String (fun _ -> ()),
     "<dir> Specifies path to 'ocaml' for running configure script";
   "-profile", arg_profile,
-    Profiles.doc
+    Profiles.doc;
+  "-embed-date", arg_bool (fun p embed_date -> { p with embed_date}),
+    "(yes|no) embeds the configure date into the coqc binary (default yes)"
+
 ]
 
 let parse_args () =
@@ -1073,6 +1079,7 @@ let write_configml f =
   let o = open_out f in
   let pr s = fprintf o s in
   let pr_s = pr "let %s = %S\n" in
+  let pr_o n x = let s = match x with None -> "None" | Some s -> "(Some " ^ "\"" ^ s ^ "\")" in pr "let %s = %s\n" n s in
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
   let pr_i32 = pr "let %s = %dl\n" in
@@ -1096,8 +1103,8 @@ let write_configml f =
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
   pr_li "caml_version_nums" caml_version_nums;
-  pr_s "date" short_date;
-  pr_s "compile_date" full_date;
+  pr_o "date" (if !prefs.embed_date then Some short_date else None);
+  pr_o "compile_date" (if !prefs.embed_date then Some full_date else None);
   pr_s "arch" arch;
   pr_b "arch_is_win32" arch_is_win32;
   pr_s "exec_extension" exe;

sysinit/usage.ml

@@ -10,8 +10,9 @@
 
 let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
-    Coq_config.version Coq_config.date;
-  Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
+    Coq_config.version (Option.default "n/d" Coq_config.date);
+  Printf.printf "compiled on %s with OCaml %s\n"
+    (Option.default "n/d" Coq_config.compile_date) Coq_config.caml_version
 
 let machine_readable_version () =
   Printf.printf "%s %s\n"

toplevel/coqtop.ml

@@ -24,12 +24,13 @@ let get_version_date () =
     let ver = input_line ch in
     let rev = input_line ch in
     let () = close_in ch in
-    (ver,rev)
+    (ver,Some rev)
   with e when CErrors.noncritical e ->
     (Coq_config.version,Coq_config.date)
 
 let print_header () =
   let (ver,rev) = get_version_date () in
+  let rev = Option.default "n/d" rev in
   Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()