Commit e08ac9fb authored by MARCHE Claude's avatar MARCHE Claude

why3replayer: option -obsolete-only

parent 9b4ab10a
* marks an incompatible change
o [why3replayer] option -obsolete-only
o workaround for a bug about modulo operator in Alt-Ergo 0.94
o fixed a consistency issue with set.Fset theory
o co-inductive predicates
......
......@@ -57,6 +57,22 @@
=========== Middle-term roadmap ==========================================
* replayer
** DONE option pour ne rejouer que si obsolete
** deplacer option -bench dans une commande de why3session
* Sortie PVS
** avec mecanisme de realization
* Yices 2 ? interesserait Cesar
* Projets interessant Cesar ?
** Preuve de prog flottants avec Frama-C+WP+Why3+PVS
** Generation d'annotations
** porter multirounding a jessie->Why3. Completer le mode full et faire passer
interval_arith.c. Completer la galerie
** preuve sur l'assembleur
* PRIORITAIRE, JCF et ANDREI, clone de module
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
......@@ -118,7 +134,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* detect editors
*** check if coqide and also emacs/proof-general is installed
* deplacer option -bench de why3replayer dans une commande de why3session
......
......@@ -456,7 +456,9 @@ option \verb|-force| described below.
\item Option \verb|-s| suppresses the output of the final tree view.
\item Option \texttt{-I \textsl{<path>}} adds \texttt{\textsl{<path>}} to the loadpath.
\item Option \verb|-force| enforces saving the session, if all proof
attempts replayed correctly, even if some goals are not proved.
attempts replayed correctly, even if some goals are not proved.
\item Option \verb|-obsolete-only| replays the proofs only if the session
is obsolete.
\item Option \texttt{-smoke-detector \{none|top|deep\}} tries to detect
if the context is self-contradicting.
\end{itemize}
......
<?xml version="1.0" encoding="UTF-8"?>
<<<<<<< HEAD
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
=======
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
>>>>>>> why3replayer: option -obsolete-only
<why3session
name="programs/add_list/why3session.xml">
<prover
......@@ -48,7 +52,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -56,7 +60,11 @@
memlimit="1000"
obsolete="false"
archived="false">
<<<<<<< HEAD
<result status="valid" time="0.00"/>
=======
<result status="valid" time="0.01"/>
>>>>>>> why3replayer: option -obsolete-only
</proof>
<proof
prover="2"
......
......@@ -5,6 +5,9 @@ case "$1" in
"-force")
REPLAYOPT="-force"
;;
"-obsolete-only")
REPLAYOPT="-obsolete-only -force"
;;
"")
REPLAYOPT=""
;;
......
......@@ -28,9 +28,7 @@ let file = ref None
let opt_version = ref false
let opt_stats = ref true
let opt_force = ref false
(*
let opt_convert_unknown_provers = ref false
*)
let opt_obsolete_only = ref false
let opt_bench = ref false
(** {2 Smoke detector} *)
......@@ -72,6 +70,9 @@ let spec = Arg.align [
("-force",
Arg.Set opt_force,
" enforce saving the session after replay") ;
("-obsolete-only",
Arg.Set opt_obsolete_only,
" replay only if session is obsolete") ;
("-smoke-detector",
Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
" try to detect if the context is self-contradicting") ;
......@@ -436,6 +437,12 @@ let () =
M.update_session ~allow_obsolete:true session env config
in
eprintf " done.@.";
if !opt_obsolete_only && not found_obs then
begin
eprintf "Session is not obsolete, hence no replayed@.";
printf "@.";
exit 0
end;
if !opt_bench then run_as_bench env_session;
let () = transform_smoke env_session in
let sched =
......
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