From f173d3289ea1b90d0b3eb009c9e11cb24428c7d7 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Sat, 18 Dec 2010 13:08:05 +0100 Subject: [PATCH] add version-printing option + set VERSION to 0.63 --- Version | 2 +- src/bench/whybench.ml | 15 +++++++++++++-- src/config/whyconfig.ml | 15 +++++++++++++-- src/ide/gconfig.ml | 2 +- src/ide/gmain.ml | 18 +++++++++++++++++- src/main.ml | 14 ++++++++++++-- 6 files changed, 57 insertions(+), 9 deletions(-) diff --git a/Version b/Version index fa73224b9..6e922f098 100644 --- a/Version +++ b/Version @@ -1,2 +1,2 @@ # Why version -VERSION=0.10 +VERSION=0.63 diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index 706666471..c921f0960 100644 --- a/src/bench/whybench.ml +++ b/src/bench/whybench.ml @@ -33,6 +33,9 @@ let usage_msg = sprintf [-P ]..." (Filename.basename Sys.argv.(0)) +let version_msg = sprintf "Why3 bench tool, version %s (build date: %s)" + Config.version Config.builddate + let opt_queue = Queue.create () let opt_input = ref None @@ -109,6 +112,7 @@ let opt_list_metas = ref false let opt_list_flags = ref false let opt_debug_all = ref false +let opt_version = ref false let opt_quiet = ref false @@ -183,7 +187,10 @@ let option_list = Arg.align [ " Set all debug flags (except parse_only and type_only)"; "--debug", Arg.String add_opt_debug, " Set a debug flag"; - "--quiet", Arg.Set opt_quiet, " Print only what asked" + "--quiet", Arg.Set opt_quiet, + " Print only what asked"; + "--version", Arg.Set opt_version, + " Print version information" ] let tools = ref [] @@ -215,6 +222,10 @@ let () = (** listings*) let opt_list = ref false in + if !opt_version then begin + opt_list := true; + printf "%s@." version_msg + end; if !opt_list_transforms then begin opt_list := true; printf "@[Known non-splitting transformations:@\n%a@]@\n@." @@ -222,7 +233,7 @@ let () = (List.sort String.compare (Trans.list_transforms ())); printf "@[Known splitting transformations:@\n%a@]@\n@." (Pp.print_list Pp.newline Pp.string) - (List.sort String.compare (Trans.list_transforms_l ())); + (List.sort String.compare (Trans.list_transforms_l ())) end; if !opt_list_printers then begin opt_list := true; diff --git a/src/config/whyconfig.ml b/src/config/whyconfig.ml index f1c6a1da2..4e29a8abd 100644 --- a/src/config/whyconfig.ml +++ b/src/config/whyconfig.ml @@ -27,11 +27,16 @@ let usage_msg = $WHY3LIB and $WHYDATA are used only when a configuration file is created" (Filename.basename Sys.argv.(0)) +let version_msg = sprintf + "Why3 configuration utility, version %s (build date: %s)" + Config.version Config.builddate + (* let libdir = ref None *) (* let datadir = ref None *) let conf_file = ref None let autoprovers = ref false let autoplugins = ref false +let opt_version = ref false let save = ref true @@ -54,9 +59,11 @@ let option_list = Arg.align [ "--autodetect-plugins", Arg.Set autoplugins, " autodetect the plugins in the default library directories"; "--install-plugin", Arg.String add_plugin, - "install a plugin to the actual libdir"; + " install a plugin to the actual libdir"; "--dont-save", Arg.Clear save, - "dont modify the config file" + " dont modify the config file"; + "--version", Arg.Set opt_version, + " print version information" ] let anon_file _ = Arg.usage option_list usage_msg; exit 1 @@ -94,6 +101,10 @@ let plugins_auto_detection config = let () = Arg.parse option_list anon_file usage_msg; + if !opt_version then begin + printf "%s@." version_msg; + exit 0 + end; let config = try read_config !conf_file with Not_found -> diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 7fc904c3f..55b75ba71 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -299,7 +299,7 @@ let show_about_window () = "Andrei Paskevich" ] ~copyright:"Copyright 2010 Univ Paris-Sud, CNRS, INRIA" - ~license:"Gnu Lesser General Public License" + ~license:"GNU Lesser General Public License" ~website:"https://gforge.inria.fr/projects/why3" ~website_label:"Project web site" ~version:Config.version diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 5a7e334e8..c38f610a1 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -92,6 +92,7 @@ open Gconfig let includes = ref [] let file = ref None +let opt_version = ref false let spec = Arg.align [ ("-I", @@ -102,9 +103,18 @@ let spec = Arg.align [ Arg.String (fun s -> input_files := s :: !input_files), " add file f to the project (ignored if it is already there)") ; *) + ("-v", + Arg.Set opt_version, + " print version information") ; ] -let usage_str = "whydb [options] [|]" +let version_msg = sprintf "Why3 IDE, version %s (build date: %s)" + Config.version Config.builddate + +let usage_str = sprintf + "Usage: %s [options] [|]" + (Filename.basename Sys.argv.(0)) + let set_file f = match !file with | Some _ -> raise (Arg.Bad "only one parameter") @@ -113,6 +123,12 @@ let set_file f = match !file with let () = Arg.parse spec set_file usage_str +let () = + if !opt_version then begin + printf "%s@." version_msg; + exit 0 + end + let fname = match !file with | None -> Arg.usage spec usage_str; diff --git a/src/main.ml b/src/main.ml index 8bb70464a..2fbaeda03 100644 --- a/src/main.ml +++ b/src/main.ml @@ -30,6 +30,9 @@ let usage_msg = sprintf "Usage: %s [options] [[file|-] [-T [-G ]...]...]..." (Filename.basename Sys.argv.(0)) +let version_msg = sprintf "Why3 platform, version %s (build date: %s)" + Config.version Config.builddate + let opt_queue = Queue.create () let opt_input = ref None @@ -109,6 +112,7 @@ let opt_list_flags = ref false let opt_parse_only = ref false let opt_type_only = ref false let opt_debug_all = ref false +let opt_version = ref false let option_list = Arg.align [ "-", Arg.Unit (fun () -> add_opt_file "-"), @@ -186,7 +190,9 @@ let option_list = Arg.align [ "--debug-all", Arg.Set opt_debug_all, " Set all debug flags (except parse_only and type_only)"; "--debug", Arg.String add_opt_debug, - " Set a debug flag" ] + " Set a debug flag"; + "--version", Arg.Set opt_version, + " Print version information" ] let () = try @@ -218,6 +224,10 @@ let () = (** listings*) let opt_list = ref false in + if !opt_version then begin + opt_list := true; + printf "%s@." version_msg + end; if !opt_list_transforms then begin opt_list := true; printf "@[Known non-splitting transformations:@\n%a@]@\n@." @@ -225,7 +235,7 @@ let () = (List.sort String.compare (Trans.list_transforms ())); printf "@[Known splitting transformations:@\n%a@]@\n@." (Pp.print_list Pp.newline Pp.string) - (List.sort String.compare (Trans.list_transforms_l ())); + (List.sort String.compare (Trans.list_transforms_l ())) end; if !opt_list_printers then begin opt_list := true; -- GitLab