why3replayer: renamed options

parent 364cc1a9
* marks an incompatible change
* [why3replayer] renamed option -obsolete-only to --obsolete-only,
-smoke-detector to --smoke-detector, -force to --force
* [library] fixed inconsistency in libraries map.MapPermut and
array.ArrayPermut; names and meaning of symbols "permut..." have
been modified
......
......@@ -559,11 +559,11 @@ Options are:
\item[\texttt{-s}] suppresses the output of the final tree view.
\item[\texttt{-q}] runs quietly (no progress info).
\item[\texttt{-I \textsl{<dir>}}] adds the given directory to the load path.
\item[\texttt{-force}] enforces saving the session, if all proof
\item[\texttt{-{}-force}] enforces saving the session, if all proof
attempts replayed correctly, even if some goals are not proved.
\item[\texttt{-obsolete-only}] replays the proofs only if the session
\item[\texttt{-{}-obsolete-only}] replays the proofs only if the session
contains obsolete proof attempts.
\item[\texttt{-smoke-detector \{none|top|deep\}}] tries to detect
\item[\texttt{-{}-smoke-detector \{none|top|deep\}}] tries to detect
if the context is self-contradicting.
\end{description}
......
......@@ -5,11 +5,11 @@ REPLAYOPT=""
while test $# != 0; do
case "$1" in
"-force")
REPLAYOPT="$REPLAYOPT -force"
"--force")
REPLAYOPT="$REPLAYOPT --force"
;;
"-obsolete-only")
REPLAYOPT="$REPLAYOPT -obsolete-only"
"--obsolete-only")
REPLAYOPT="$REPLAYOPT --obsolete-only"
;;
"--prover")
REPLAYOPT="$REPLAYOPT --prover $2"
......@@ -28,7 +28,7 @@ TMPERR=$PWD/why3regtests.err
cd `dirname $0`
# too early to do that
# REPLAYOPT="$REPLAYOPT -smoke-detector top"
# REPLAYOPT="$REPLAYOPT --smoke-detector top"
res=0
export success=0
......
......@@ -82,13 +82,13 @@ let spec = Arg.align [
" same as -C") ;
("--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
"<file> Read additional configuration from <file>") ;
("-force",
("--force",
Arg.Set opt_force,
" enforce saving the session after replay") ;
("-obsolete-only",
("--obsolete-only",
Arg.Set opt_obsolete_only,
" replay only if session is obsolete") ;
("-smoke-detector",
("--smoke-detector",
Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
" try to detect if the context is self-contradicting") ;
("--bench",
......
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