add-prover: now adds a shortcut too

CHANGES.md

@@ -7,8 +7,12 @@ Transformations
   * `destruct` now simplifies away equalities on constructors
 
 Tools
-  * add a command `why3 session update` to modify sessions from the
-    command line
+  * add a command 'why3 session update' to modify sessions from the
+    command line. So far, only one option exists, for renaming files
+    fixes issue #227
+  * option `--add-prover` of `why3 config` is now taking the shortcut as
+    second argument.  option `--list-prover-ids` renamed to
+    `--list-prover-families`. See documentation for details.
 
 IDE
   * clicking on the status of a failed proof attempt in the proof tree

doc/install.tex

@@ -151,10 +151,14 @@ use specialized executable names, such as \texttt{cvc4-1.4} or
 added to the \texttt{config} command to specify names of prover executables, \eg
 \index{add-prover@\verb+--add-prover+}
 \begin{verbatim}
-why3 config --add-prover cvc4 /usr/local/bin/cvc4-dev
+why3 config --add-prover cvc4 cvc4-dev /usr/local/bin/cvc4-dev
 \end{verbatim}
-the first argument (here \verb|cvc4|) must be one of the class of
-provers known in the file \verb|provers-detection-data.conf| typically
+the first argument (here \verb|cvc4|) must be one of the family of
+provers known. The list of these famillies can be obtain using
+\begin{verbatim}
+why3 config --list-prover-families
+\end{verbatim}
+as they are in fact listed in the file \verb|provers-detection-data.conf|, typically
 located in \verb|/usr/local/share/why3| after installation. See
 Appendix~\ref{sec:proverdetecttiondata} for details.
 

doc/manpages.tex

@@ -129,13 +129,13 @@ the option \verb|--add-prover| will add a specified binary
 to the configuration. For example, an Alt-Ergo executable
 \verb|/home/me/bin/alt-ergo-trunk| can be added as follows:
 \begin{verbatim}
-why3 config --add-prover alt-ergo /home/me/bin/alt-ergo-trunk
+why3 config --add-prover alt-ergo alt-ergo-trunk /home/me/bin/alt-ergo-trunk
 \end{verbatim}
-As the first argument, one should put a prover
-identification string. The list of known prover identifiers
-can be obtained by the option \verb|--list-prover-ids|.
+As the first argument, one should put a prover family
+identification string. The list of known prover families
+can be obtained by the option \verb|--list-prover-families|.
 \index{add-prover@\verb+--add-prover+}
-\index{list-prover-ids@\verb+--list-prover-ids+}
+\index{list-prover-ids@\verb+--list-prover-families+}
 
 \section{The \texttt{prove} Command}
 \label{sec:why3ref}

src/driver/autodetection.ml

@@ -566,7 +566,7 @@ let run_auto_detection config =
   let config = set_provers config detected in
   config
 
-let list_prover_ids () =
+let list_prover_families () =
   let config = default_config "" in
   let main = get_main config in
   let l,_ = read_auto_detection_data main in
@@ -598,12 +598,20 @@ let add_existing_shortcuts env shortcuts =
   in
   Mstr.iter aux shortcuts
 
-let add_prover_binary config id path =
+let add_prover_binary config id shortcut path =
   let main = get_main config in
   let l,env = read_auto_detection_data main in
-  add_existing_shortcuts env (get_prover_shortcuts config);
+  let prover_shortcuts = get_prover_shortcuts config in
+  if Mstr.mem shortcut prover_shortcuts then
+    Loc.errorm "Shortcut %s already in use" shortcut;
+  add_existing_shortcuts env prover_shortcuts;
   let l = List.filter (fun p -> p.prover_id = id) l in
-  if l = [] then Loc.errorm "Unknown prover id: %s" id;
+  if l = [] then begin
+    let list_of_allowed_id =
+      Format.asprintf "@[<hov 2>Known prover families:@\n%a@]@\n@."
+        (Pp.print_list Pp.newline Pp.string)
+        (List.sort String.compare (list_prover_families ())) in
+    Loc.errorm "Unknown prover id: %s\n%s" id list_of_allowed_id end;
   let detected = List.fold_left
     (fun acc data -> detect_exec env data acc path) Mprover.empty l in
   let detected = detect_unknown env detected in
@@ -622,6 +630,7 @@ let add_prover_binary config id path =
     let p = {p with prover = prover_id} in
     add_prover_with_uniq_id p provers in
   let provers = Mprover.fold fold detected provers in
-  let shortcuts = convert_shortcuts env in
+  let prover = fst (Mprover.choose detected) in
+  let shortcuts = Mstr.add shortcut prover (convert_shortcuts env) in
   let config = set_provers config ~shortcuts provers in
   config

src/driver/autodetection.mli

@@ -9,11 +9,12 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** Lists prover id strings from detection config *)
-val list_prover_ids : unit -> string list
+(** Lists prover family names from detection config *)
+val list_prover_families : unit -> string list
 
 (** Adds a new prover executable *)
-val add_prover_binary : Whyconf.config -> string -> string -> Whyconf.config
+val add_prover_binary :
+  Whyconf.config -> string -> string -> string -> Whyconf.config
 
 (** Replace the provers by autodetected one *)
 val run_auto_detection : Whyconf.config -> Whyconf.config

src/tools/why3config.ml

@@ -26,7 +26,7 @@ let autoprovers = ref false
 let autoplugins = ref false
 let resetloadpath = ref false
 
-let opt_list_prover_ids = ref false
+let opt_list_prover_families = ref false
 
 let save = ref true
 
@@ -54,10 +54,12 @@ let option_list = Arg.align [
   " search for both provers and plugins, and resets the default loadpath";
   "--add-prover", Arg.Tuple
     (let id = ref "" in
+     let shortcut = ref "" in
      [Arg.Set_string id;
-      Arg.String (fun name -> Queue.add (!id, name) prover_bins)]),
-  "<id><file> add a new prover executable";
-  "--list-prover-ids", Arg.Set opt_list_prover_ids,
+      Arg.Set_string shortcut;
+      Arg.String (fun name -> Queue.add (!id, !shortcut, name) prover_bins)]),
+  "<id> <shortcut> <file> add a new prover executable";
+  "--list-prover-families", Arg.Set opt_list_prover_families,
   " list known prover families";
   "--install-plugin", Arg.String add_plugin,
   "<file> install a plugin to the actual libdir";
@@ -70,8 +72,8 @@ let option_list = Arg.align [
 
 let anon_file _ = Arg.usage option_list usage_msg; exit 1
 
-let add_prover_binary config (id,file) =
-  Autodetection.add_prover_binary config id file
+let add_prover_binary config (id,shortcut,file) =
+  Autodetection.add_prover_binary config id shortcut file
 
 let install_plugin main p =
   begin match Plugin.check_plugin p with
@@ -127,11 +129,11 @@ let main () =
   (* Debug flag *)
   Debug.Args.set_flags_selected ();
 
-  if !opt_list_prover_ids then begin
+  if !opt_list_prover_families then begin
     opt_list := true;
     printf "@[<hov 2>Known prover families:@\n%a@]@\n@."
       (Pp.print_list Pp.newline Pp.string)
-      (List.sort String.compare (Autodetection.list_prover_ids ()))
+      (List.sort String.compare (Autodetection.list_prover_families ()))
   end;
 
   opt_list :=  Debug.Args.option_list () || !opt_list;