Commit 6793ee63 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

better syntax for --add-prover

parent 1efd7a6d
......@@ -133,9 +133,9 @@
== TODOs ==
* Document the Coq plugin and tactic
** option timelimit <n>
** renommer "coq-plugin" en "coq-tactic"
* DONE Document the Coq plugin and tactic
** DONE option timelimit <n>
** DONE renommer "coq-plugin" en "coq-tactic"
* (JCF, ANDREI) add all examples from the VSTTE 2012 competition
......@@ -148,7 +148,7 @@
- Documenter l'utilisation de plusieurs versions du meme prouveur comme CVC3 et Z3
DONE, mais reorganiser la section, lien sur la page web des prouveurs
- DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
mais remplacer le ":" par " " (Arg.Tuple)
DONE remplacer le ":" par " " (Arg.Tuple)
- (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé. Et les mettre au point:
. Lors d'un replay, le dialogue "replace proof" apparait un nombre important de fois,
il faut absolument pouvoir interrompre, ou donner une reponse qui soit appliquée pour le reste.
......@@ -12,8 +12,8 @@ The Coq tactic is installed in
where \textit{why3-lib-dir} is \why's library directory, that is typically
\texttt{/usr/lib/why3} or \texttt{/usr/local/lib/why3}. This directory
where \textit{why3-lib-dir} is \why's library directory, as reported
by \verb+why3 --print-libdir+. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3ide}, \texttt{why3replayer},
etc.). If you are calling Coq by yourself, you need to add
......@@ -32,7 +32,8 @@ The Coq tactic is called \texttt{why3} and is used as follows:
$[$\texttt{timelimit} \textit{n}$]$.
The string \textit{prover-name} identifies one of the automated theorem provers
supported by \why, as reported by \verb+why3 --list-provers+.
supported by \why, as reported by \verb+why3 --list-provers+
(interactive provers excluded).
The current goal is then translated to \why's logic and the prover is
called. If it reports the goal to be valid, then Coq's \texttt{admit}
tactic is used to assume the goal. The prover is called with a time
......@@ -181,9 +181,9 @@ 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:
why3config --add-prover alt-ergo:/home/me/bin/alt-ergo-trunc
why3config --add-prover alt-ergo /home/me/bin/alt-ergo-trunc
To the left of the colon \verb|:| one should put a prover
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|.
......@@ -78,7 +78,7 @@ _why3()
return 0
ids=$($1 --list-prover-ids | grep -v '^Known \|^$' | sed -e 's/$/:/')
ids=$($1 --list-prover-ids | grep -v '^Known \|^$')
COMPREPLY=( $(compgen -W "$ids" -- "$cur") )
return 0
......@@ -48,18 +48,6 @@ let set_oref r = (fun s -> r := Some s)
let prover_bins = Queue.create ()
let add_prover arg =
let res =
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
Queue.add res prover_bins
let plugins = Queue.create ()
let add_plugin x = Queue.add x plugins
......@@ -78,8 +66,11 @@ 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";
"--add-prover", Arg.Tuple
(let id = 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,
" List known prover families";
"--install-plugin", Arg.String add_plugin,
Supports Markdown
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