why3config: --add-prover option

ROADMAP

@@ -126,7 +126,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
 
 == TODOs ==
 
-* (JCF, ANDREI) add all examples from the VSTTE 2012 competition 
+* (JCF, ANDREI) add all examples from the VSTTE 2012 competition
 
 * Documentation
  - (GUILLAUME) Realisations Coq, comment fait l'utilisateur pour faire ses realisations
@@ -135,7 +135,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
  - (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
  - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé
    ET LES METTRE AU POINT
- - (ANDREI) ajouter option a why3config pour ajouter association ident-executable
+ - DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
  - (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
  - (WHO?) complete api.tex: explain how to build theories, apply
    transformations, write new functions on terms (A)

doc/manpages.tex

@@ -117,15 +117,15 @@ Section~\ref{sec:why3config}.
 \label{sec:why3config}
 
 \why must be configured to access external provers. Typically, this is done
-by running either the command line tool
-\begin{verbatim}
-why3config
-\end{verbatim}
-or using the menu
-\begin{verbatim}
-File/Detect provers
-\end{verbatim}
-of the IDE. This must be redone each time a new prover is installed.
+by running
+%%either
+the command line tool \texttt{why3config}.
+%%or using the menu
+%%\begin{verbatim}
+%%File/Detect provers
+%%\end{verbatim}
+%%of the IDE.
+This must be redone each time a new prover is installed.
 
 The provers which \why attempts to detect are described in
 the readable configuration file \texttt{provers-detection-data.conf}
@@ -170,6 +170,18 @@ The option \verb|--detect-provers| should be used to force
 provers and to replace them in the configuration file. The option
 \verb|--detect-plugins| will do the same for plugins.
 
+If a supported prover is installed under a name
+that is not automatically recognized by \texttt{why3config},
+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-trunc| can be added as follows:
+\begin{verbatim}
+why3config --add-prover alt-ergo:/home/me/bin/alt-ergo-trunc
+\end{verbatim}
+To the left of the colon \verb|:| one should put a prover
+identification string. The list of known prover identifiers
+can be obtained by the option \verb|--list-prover-ids|.
+
 \section{The \texttt{why3} command-line tool}
 \label{sec:why3ref}
 

share/bash/why3

@@ -77,6 +77,11 @@ _why3()
             _filedir
             return 0
             ;;
+        --add-prover)
+            ids=$($1 --list-prover-ids | grep -v '^Known \|^$' | sed -e 's/$/:/')
+            COMPREPLY=( $(compgen -W "$ids" -- "$cur") )
+            return 0
+            ;;
         -smoke-detector|--smoke-detector)
             COMPREPLY=( $( compgen -W 'none top deep' -- "$cur" ) )
             return 0
@@ -86,7 +91,6 @@ _why3()
             COMPREPLY=( $( compgen -W "$flags" -- "$cur" ) )
             return 0
             ;;
-# Why3session options
         --filter-prover)
             provers=$(${1/session/} --list-provers | grep -v '^Known ' | cut -d ' ' -f 3)
             COMPREPLY=( $( compgen -W "$provers" -- "$cur" ) )

src/config/whyconfig.ml

@@ -39,10 +39,26 @@ let autoprovers = ref false
 let autoplugins = ref false
 let opt_version = ref false
 
+let opt_list_prover_ids = ref false
+
 let save = ref true
 
 let set_oref r = (fun s -> r := Some s)
 
+let prover_bins = Queue.create ()
+
+let add_prover arg =
+  let res =
+    try
+      let index = String.index arg ':' in
+      (String.sub arg 0 index),
+      (String.sub arg (index+1) (String.length arg - (index + 1)))
+    with Not_found ->
+      eprintf "Error: provide a path to the prover binary.@.";
+      exit 1
+  in
+  Queue.add res prover_bins
+
 let plugins = Queue.create ()
 let add_plugin x = Queue.add x plugins
 
@@ -61,8 +77,12 @@ let option_list = Arg.align [
   " Search for plugins in the default library directory";
   "--detect", Arg.Unit (fun () -> autoprovers := true; autoplugins := true),
   " Search for both provers and plugins";
+  "--add-prover", Arg.String add_prover,
+  "<id>:<file> Add a new prover executable";
+  "--list-prover-ids", Arg.Set opt_list_prover_ids,
+  " List known prover families";
   "--install-plugin", Arg.String add_plugin,
-  " Install a plugin to the actual libdir";
+  "<file> Install a plugin to the actual libdir";
   "--dont-save", Arg.Clear save,
   " Do not modify the config file";
   Debug.Opt.desc_debug_list;
@@ -74,6 +94,9 @@ 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 install_plugin main p =
   begin match Plugin.check_plugin p with
     | Plugin.Plubad ->
@@ -128,6 +151,13 @@ let main () =
   (** Debug flag *)
   Debug.Opt.set_flags_selected ();
 
+  if !opt_list_prover_ids 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 ()))
+  end;
+
   opt_list :=  Debug.Opt.option_list () || !opt_list;
   if !opt_list then exit 0;
 
@@ -150,6 +180,9 @@ let main () =
      !datadir in *)
   let main = try Queue.fold install_plugin main plugins with Exit -> exit 1 in
   let config = set_main config main in
+  let config =
+    try Queue.fold add_prover_binary config prover_bins with Exit -> exit 1 in
+
   let conf_file = get_conf_file config in
   if not (Sys.file_exists conf_file) then begin
     autoprovers := true;

src/driver/autodetection.ml

@@ -81,12 +81,9 @@ let read_auto_detection_data main =
     load rc
   with
     | Failure "lexing" ->
-        eprintf "Syntax error in provers-detection-data.conf@.";
-        exit 2
+        Loc.errorm "Syntax error in provers-detection-data.conf@."
     | Not_found ->
-        eprintf "provers-detection-data.conf not found at %s@." filename;
-        exit 2
-
+        Loc.errorm "provers-detection-data.conf not found at %s@." filename
 
 let provers_found = ref 0
 
@@ -178,7 +175,6 @@ let detect_exec main data com =
       end
 
 let detect_prover main acc l =
-  let prover_id = (List.hd l).prover_id in
   try
     let detect_execs data =
       try Some (Util.list_first (detect_exec main data) data.execs)
@@ -187,7 +183,7 @@ let detect_prover main acc l =
     let prover = Util.list_first detect_execs l in
     Mprover.add prover.prover prover acc
   with Not_found ->
-    eprintf "Prover %s not found.@." prover_id;
+    eprintf "Prover %s not found.@." (List.hd l).prover_id;
     acc
 (* does not work
   List.fold_left
@@ -211,3 +207,22 @@ let run_auto_detection config =
   let length = Mprover.cardinal detect in
   eprintf "%d provers detected.@." length;
   set_provers config detect
+
+let list_prover_ids () =
+  let config = default_config "/dev/null" in
+  let main = get_main config in
+  let l = read_auto_detection_data main in
+  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
+  Sstr.elements s
+
+let add_prover_binary config id path =
+  let main = get_main config in
+  let l = read_auto_detection_data main in
+  let l = List.filter (fun p -> p.prover_id = id) l in
+  if l = [] then Loc.errorm "Unknown prover id: %s" id;
+  let p = try
+    Util.list_first (fun d -> detect_exec main d path) (List.rev l)
+  with Not_found ->
+    Loc.errorm "File %s does not correspond to the prover id %s" path id
+  in
+  set_provers config (Mprover.add p.prover p (get_provers config))

src/driver/autodetection.mli

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