diff --git a/config/coq_config.mli b/config/coq_config.mli index 809fa3d758ad6..84d5496697302 100644 --- a/config/coq_config.mli +++ b/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 diff --git a/config/dune b/config/dune index 83d1364b0c267..30ba11d8ab795 100644 --- a/config/dune +++ b/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)))) diff --git a/configure.ml b/configure.ml index 40d77ed1097f9..f62954f14a542 100644 --- a/configure.ml +++ b/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,6 +297,7 @@ let default = { force_caml_version = false; force_findlib_version = false; warn_error = false; + embed_date = true; } let devel state = { state with @@ -303,8 +305,9 @@ let devel state = { state with 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 _ -> ()), " 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; diff --git a/sysinit/usage.ml b/sysinit/usage.ml index 763cd54137c17..5892f9087a073 100644 --- a/sysinit/usage.ml +++ b/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" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 16028be9101c0..78f35d299ccd7 100644 --- a/toplevel/coqtop.ml +++ b/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 ()