add version-printing option + set VERSION to 0.63

Version

 # Why version
-VERSION=0.10
+VERSION=0.63

src/bench/whybench.ml

@@ -33,6 +33,9 @@ let usage_msg = sprintf
   [-P <prover> ]..."
   (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,
       "<flag> 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 "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
@@ -222,7 +233,7 @@ let () =
       (List.sort String.compare (Trans.list_transforms ()));
     printf "@[<hov 2>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;

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 ->

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

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),
    "<f> 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] [<file.why>|<project directory>]"
+let version_msg = sprintf "Why3 IDE, version %s (build date: %s)"
+  Config.version Config.builddate
+
+let usage_str = sprintf
+  "Usage: %s [options] [<file.why>|<project directory>]"
+  (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;

src/main.ml

@@ -30,6 +30,9 @@ let usage_msg = sprintf
   "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
   (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,
-      "<flag> Set a debug flag" ]
+      "<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 "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
@@ -225,7 +235,7 @@ let () =
       (List.sort String.compare (Trans.list_transforms ()));
     printf "@[<hov 2>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;