diff options
| -rw-r--r-- | checker/checker.ml | 14 | ||||
| -rw-r--r-- | config/coq_config.mli | 2 | ||||
| -rw-r--r-- | configure.ml | 27 | ||||
| -rw-r--r-- | ide/coqide/coq.ml | 21 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 4 | ||||
| -rw-r--r-- | sysinit/usage.ml | 5 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 10 |
8 files changed, 22 insertions, 64 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index bdfc5f07be..3a16b7f407 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -48,19 +48,17 @@ let path_of_string s = let ( / ) = Filename.concat -let get_version_date () = +let get_version () = 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) - with _ -> (Coq_config.version,Coq_config.date) + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let print_header () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; - flush stdout + Printf.printf "Welcome to Chicken %s\n%!" (get_version ()) (* Adding files to Coq loadpath *) @@ -170,9 +168,7 @@ let compile_files senv = ~check:(List.rev !compile_list) 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; + Printf.printf "The Coq Proof Checker, version %s\n" Coq_config.version; exit 0 (* print the usage of coqtop (or coqc) on channel co *) diff --git a/config/coq_config.mli b/config/coq_config.mli index 809fa3d758..035574475d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -33,8 +33,6 @@ 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 vo_version : int32 val state_magic_number : int diff --git a/configure.ml b/configure.ml index 40d77ed109..7814204e42 100644 --- a/configure.ml +++ b/configure.ml @@ -196,31 +196,6 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false -let build_date = - try - float_of_string (Sys.getenv "SOURCE_DATE_EPOCH") - with - Not_found -> Unix.time () - -(** * Date *) - -(** The short one is displayed when starting coqtop, - The long one is used as compile date *) - -let months = - [| "January";"February";"March";"April";"May";"June"; - "July";"August";"September";"October";"November";"December" |] - -let get_date () = - let now = Unix.gmtime build_date in - let year = 1900+now.Unix.tm_year in - let month = months.(now.Unix.tm_mon) in - sprintf "%s %d" month year, - sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year - now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec - -let short_date, full_date = get_date () - (** * Command-line parsing *) type ide = Opt | Byte | No @@ -1096,8 +1071,6 @@ 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_s "arch" arch; pr_b "arch_is_win32" arch_is_win32; pr_s "exec_extension" exe; diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index b8228df2aa..20e9f0134f 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -13,13 +13,9 @@ open Preferences let ideslave_coqtop_flags = ref None -(** * Version and date *) +(** * Version *) -let get_version_date () = - let date = - if Glib.Utf8.validate Coq_config.date - then Coq_config.date - else "<date not printable>" in +let get_version () = try (* the following makes sense only when running with local layout *) let coqroot = Filename.concat @@ -29,21 +25,20 @@ let get_version_date () = let ch = open_in (Filename.concat coqroot "revision") in let ver = input_line ch in let rev = input_line ch in - (ver,rev) - with _ -> (Coq_config.version,date) + close_in ch; + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let short_version () = - let (ver,date) = get_version_date () in - Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date + Printf.sprintf "The Coq Proof Assistant, version %s\n" (get_version ()) let version () = - let (ver,date) = get_version_date () in Printf.sprintf - "The Coq Proof Assistant, version %s (%s)\ + "The Coq Proof Assistant, version %s\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ \nThis is %s \n" - ver date + (get_version ()) Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (Filename.basename Sys.executable_name) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index b42c705add..a0a8b71ead 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -397,8 +397,8 @@ let set_options options = 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 = "n/a"; + Interface.compile_date = "n/a"; } let handle_exn (e, info) = diff --git a/sysinit/usage.ml b/sysinit/usage.ml index 763cd54137..d00b916f23 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -9,9 +9,8 @@ (************************************************************************) 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 + Printf.printf "The Coq Proof Assistant, version %s\n" Coq_config.version; + Printf.printf "compiled with OCaml %s\n" Coq_config.caml_version let machine_readable_version () = Printf.printf "%s %s\n" diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 6ebf9b71d6..b8d5032373 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -87,8 +87,7 @@ let obsolete s = course). *) let banner () = - eprintf "This is coqdoc version %s, compiled on %s\n" - Coq_config.version Coq_config.compile_date; + eprintf "This is coqdoc version %s\n" Coq_config.version; flush stderr let target_full_name f = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 16028be910..13637ef540 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -18,19 +18,17 @@ let () = at_exit flush_all let ( / ) = Filename.concat -let get_version_date () = +let get_version () = 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) - with e when CErrors.noncritical e -> - (Coq_config.version,Coq_config.date) + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let print_header () = - let (ver,rev) = get_version_date () in - Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + Feedback.msg_info (str "Welcome to Coq " ++ str (get_version ())); flush_all () |