Commit c3f85da5 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch '249_why3config' into 'master'

add-prover: now adds a shortcut too

See merge request !74
parents e37ef92b e92648c9
......@@ -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
......
......@@ -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.
......
......@@ -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}
......
......@@ -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
......@@ -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
......@@ -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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment