Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
wants to merge 1 commit into from
Closed

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
11 changes: 8 additions & 3 deletions checker/checker.ml
View file
Open in desktop
Expand Up @@ -48,17 +48,19 @@ let path_of_string s =

let ( / ) = Filename.concat

(* Duplicated with coqtop.ml *)
let get_version_date () =
try
let ch = open_in (Envars.coqlib () / "revision") in
let ver = input_line ch in
let rev = input_line ch in
let () = close_in ch in
(ver,rev)
(ver,Some rev)
with _ -> (Coq_config.version,Coq_config.date)

let print_header () =
let (ver,rev) = (get_version_date ()) in
let rev = Option.default "n/a" rev in
Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
flush stdout

Expand Down Expand Up @@ -169,10 +171,13 @@ let compile_files senv =
~admit:(List.rev !admit_list)
~check:(List.rev !compile_list)

(* duplicated with usage.ml *)
let avail_version = Option.default "n/a"

let version () =
Printf.printf "The Coq Proof Checker, version %s (%s)\n"
Coq_config.version Coq_config.date;
Printf.printf "compiled on %s\n" Coq_config.compile_date;
Coq_config.version (avail_version Coq_config.date);
Printf.printf "compiled on %s\n" (avail_version Coq_config.compile_date);
exit 0

(* print the usage of coqtop (or coqc) on channel co *)
Expand Down
4 changes: 2 additions & 2 deletions config/coq_config.mli
View file
Open in desktop
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion config/dune
View file
Open in desktop
Expand Up @@ -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))))
15 changes: 11 additions & 4 deletions configure.ml
View file
Open in desktop
Expand Up @@ -259,6 +259,7 @@ type preferences = {
force_caml_version : bool;
force_findlib_version : bool;
warn_error : bool;
embed_date : bool;
}

module Profiles = struct
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 () =
Expand Down Expand Up @@ -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
Expand All @@ -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;
Expand Down
5 changes: 3 additions & 2 deletions ide/coqide/coq.ml
View file
Open in desktop
Expand Up @@ -16,9 +16,10 @@ let ideslave_coqtop_flags = ref None
(** * Version and date *)

let get_version_date () =
let coq_date = Option.default "n/a" Coq_config.date in
let date =
if Glib.Utf8.validate Coq_config.date
then Coq_config.date
if Glib.Utf8.validate coq_date
then coq_date
else "<date not printable>" in
try
(* the following makes sense only when running with local layout *)
Expand Down
6 changes: 4 additions & 2 deletions ide/coqide/idetop.ml
View file
Open in desktop
Expand Up @@ -394,11 +394,13 @@ let set_options options =
in
List.iter iter options

let avail_version = Option.default "n/a"

let about () = {
Interface.coqtop_version = Coq_config.version;
Interface.protocol_version = Xmlprotocol.protocol_version;
Interface.release_date = Coq_config.date;
Interface.compile_date = Coq_config.compile_date;
Interface.release_date = avail_version Coq_config.date;
Interface.compile_date = avail_version Coq_config.compile_date;
}

let handle_exn (e, info) =
Expand Down
7 changes: 5 additions & 2 deletions sysinit/usage.ml
View file
Open in desktop
Expand Up @@ -8,10 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

let avail_version = Option.default "n/a"

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 (avail_version Coq_config.date);
Printf.printf "compiled on %s with OCaml %s\n"
(avail_version Coq_config.compile_date) Coq_config.caml_version

let machine_readable_version () =
Printf.printf "%s %s\n"
Expand Down
4 changes: 3 additions & 1 deletion tools/coqdoc/main.ml
View file
Open in desktop
Expand Up @@ -86,9 +86,11 @@ let obsolete s =
is not (unless both standard and error outputs are redirected, of
course). *)

let avail_version = Option.default "n/a"

let banner () =
eprintf "This is coqdoc version %s, compiled on %s\n"
Coq_config.version Coq_config.compile_date;
Coq_config.version (avail_version Coq_config.compile_date);
flush stderr

let target_full_name f =
Expand Down
3 changes: 2 additions & 1 deletion toplevel/coqtop.ml
View file
Open in desktop
Expand Up @@ -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/a" rev in
Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
flush_all ()

Expand Down