Commit b160c23d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fix a problem with computation of obsolete status of a session

(in case of a prover upgrade)
parent 1ce76bcc
......@@ -192,8 +192,8 @@ means. A session stores which file you prove, by applying which
transformations, by using which prover. A proof attempt records the
complete name of a prover (name, version, optional attribute), the
time limit and memory limit given, and the result of the prover. The
result of the prover is the same than when you run the why3 tool. It
contain the time taken and the state of the proof:
result of the prover is the same as when you run the why3 tool. It
contains the time taken and the state of the proof:
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover. The
......@@ -229,8 +229,11 @@ transformations have changed (new version of why3) why3 will detect
that. The provers will perhaps answer differently on this new
problems. So the proof attempts that corresponds to a goal that
changed are marked obsolete. We say that a session is obsolete if new
goals are made obsolete by this method during start-up. A session can
be not obsolete even if it contains obsolete goals.
goals are made obsolete by this method during start-up.
% Claude: Alors la je ne vois pas pourquoi
% A session can
% be not obsolete even if it contains obsolete goals.
\subsection{Left toolbar actions}
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="examples/programs/mjrty/why3session.xml" shape_version="2">
name="programs/mjrty/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -24,13 +24,13 @@
expanded="true">
<theory
name="Mjrty"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="23" loccnumb="7" loccnume="12"
verified="true"
expanded="true">
<goal
name="WP_parameter mjrty"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="parameter mjrty"
sum="e25d8323230273b74d0043172b17e49a"
......@@ -45,7 +45,7 @@
expanded="true">
<goal
name="WP_parameter mjrty.1"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="precondition"
sum="11abbb8f44baf021791769315bf5452e"
......@@ -60,12 +60,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.2"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="3790f5b09a28d0855b4cd502c7cd7509"
......@@ -80,12 +80,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.3"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="b7dfa3b0d8ba694dfeb04745cb9fc49b"
......@@ -105,7 +105,7 @@
</goal>
<goal
name="WP_parameter mjrty.4"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="3ce9c726f394f9ba61c441743cbf337c"
......@@ -120,12 +120,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.5"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="8a7db61c77b607e27a9266b327ba7475"
......@@ -140,12 +140,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.6"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="3ebaf28f29e5f996333794454c031c63"
......@@ -160,12 +160,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.7"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="992f27159e5d51d7d6eb43065b2458be"
......@@ -180,12 +180,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.8"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="f7bcd880f5f8a35bb58765ea429fa279"
......@@ -200,12 +200,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="1d5bfaacf10bc9e727c03a0309743e77"
......@@ -217,10 +217,10 @@
<transf
name="split_goal"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter mjrty.9.1"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="9fbdaa1fbfc16cdd5ef837ef0bcd6583"
......@@ -240,7 +240,7 @@
</goal>
<goal
name="WP_parameter mjrty.9.2"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="1b7fcc66b0ca76ac6613a0661f4b5157"
......@@ -260,7 +260,7 @@
</goal>
<goal
name="WP_parameter mjrty.9.3"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="fd9ea2fdf2f758121e9599287926f867"
......@@ -275,12 +275,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.79"/>
<result status="valid" time="1.48"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.4"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="418e35ab7e64c4e282fcaac4f0fdf2b4"
......@@ -295,12 +295,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.29"/>
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.5"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="03178ca2795f7bd2bfab41bcb0bc71d6"
......@@ -315,12 +315,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.6"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="4fccca150a2dbdd518e542dfdcc66abd"
......@@ -335,12 +335,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.7"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="654f9e448631cc2af4037737e19d39a9"
......@@ -355,12 +355,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.8"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="19c8b8a9cbbbcfb602902a631e393538"
......@@ -375,12 +375,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.66"/>
<result status="valid" time="0.22"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.9"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="3820a7185e5c2cd76f08c4b3ec9eafd7"
......@@ -395,12 +395,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.10"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="e25b4644a4eaeb67a7abb546e8da1285"
......@@ -413,9 +413,9 @@
prover="0"
timelimit="20"
memlimit="800"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="42.88"/>
<result status="timeout" time="20.07"/>
</proof>
<proof
prover="1"
......@@ -423,12 +423,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.49"/>
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.11"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="651f2780d70f5e6053f4c9ec55c9ace3"
......@@ -443,12 +443,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.12"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="05d3a1793660c528a93f56d1c46d23de"
......@@ -463,12 +463,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.13"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="d9d2638cffa6f57c4c7b72a615052f47"
......@@ -483,12 +483,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.14"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="7d1ef28579d25273688e212cf8c64c81"
......@@ -503,14 +503,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter mjrty.10"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="31d3bc4f3dac672a03a19e7f0799410a"
......@@ -525,12 +525,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.11"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="0dc9a33d14f134afc783b4d3570c40ee"
......@@ -545,12 +545,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.12"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="750de723277314d2bd3e7bb8e2bacd79"
......@@ -570,7 +570,7 @@
</goal>
<goal
name="WP_parameter mjrty.13"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop initialization"
sum="fd0b0cd944536d9ca03d1a8b72805aa9"
......@@ -585,12 +585,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="1adc713b97af66b33ee5b6aedc0245fb"
......@@ -605,7 +605,7 @@
expanded="true">
<goal
name="WP_parameter mjrty.14.1"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="36512e3aa631d00ae2052db9da934479"
......@@ -620,12 +620,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.2"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="82d1a321a8ccd61dd3e0d4904b44e692"
......@@ -640,12 +640,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="4.48"/>
<result status="valid" time="1.35"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.3"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="692d5fbcbf1f02f8796790d6be5d8bad"
......@@ -660,12 +660,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.4"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="e93f39b8fa603941b60e4b28edd4d281"
......@@ -680,12 +680,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.5"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="3015b8586c127364af3853a65eecb368"
......@@ -700,12 +700,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.6"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="56dbaa7ddf0823445924bcb0e9d73410"
......@@ -720,12 +720,12 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14.7"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="for loop preservation"
sum="2e1d3039dc853a3796c48a9449c71650"
......@@ -740,14 +740,14 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter mjrty.15"
locfile="examples/programs/mjrty/../mjrty.mlw"
locfile="programs/mjrty/../mjrty.mlw"
loclnum="38" loccnumb="6" loccnume="11"
expl="exceptional postcondition"
sum="8ab72d659235f585660c37e4a79232af"
......@@ -762,7 +762,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
......
......@@ -1941,10 +1941,14 @@ end
(* merge a file into another *)
(**********************************)
let found_obsolete = ref false
let merge_proof ~keygen obsolete to_goal _ from_proof =
let obsolete = obsolete || from_proof.proof_obsolete in
found_obsolete := obsolete || ! found_obsolete;
ignore
(add_external_proof ~keygen
~obsolete:(obsolete || from_proof.proof_obsolete)
~obsolete
~archived:from_proof.proof_archived
~timelimit:from_proof.proof_timelimit
~memlimit:from_proof.proof_memlimit
......@@ -2254,7 +2258,7 @@ let merge_theory ~keygen env ~allow_obsolete from_th to_th =
Util.Mstr.add g.goal_name.Ident.id_string g from_goals)
Util.Mstr.empty from_th.theory_goals
in
Util.list_or
List.iter
(fun to_goal ->
try
let from_goal =
......@@ -2265,12 +2269,12 @@ let merge_theory ~keygen env ~allow_obsolete from_th to_th =
dprintf debug "[Reload] Goal %s.%s has changed@\n"
to_th.theory_name.Ident.id_string
to_goal.goal_name.Ident.id_string;
if not allow_obsolete then raise OutdatedSession
if not allow_obsolete then raise OutdatedSession;
found_obsolete := true;
end;
merge_any_goal ~keygen env goal_obsolete from_goal to_goal;
goal_obsolete
merge_any_goal ~keygen env goal_obsolete from_goal to_goal
with
| Not_found when allow_obsolete -> true
| Not_found when allow_obsolete -> ()
| Not_found -> raise OutdatedSession
) to_th.theory_goals
......@@ -2282,8 +2286,7 @@ let merge_file ~keygen env ~allow_obsolete from_f to_f =
(fun acc t -> Util.Mstr.add t.theory_name.Ident.id_string t acc)
Util.Mstr.empty from_f.file_theories
in
let b =
Util.list_or
List.iter
(fun to_th ->
try
let from_th =
......@@ -2294,14 +2297,11 @@ let merge_file ~keygen env ~allow_obsolete from_f to_f =
in
merge_theory ~keygen env ~allow_obsolete from_th to_th
with
| Not_found when allow_obsolete -> true
| Not_found when allow_obsolete -> ()
| Not_found -> raise OutdatedSession
)
to_f.file_theories
in
dprintf debug "[Info] merge_file, done@\n";
b
to_f.file_theories;
dprintf debug "[Info] merge_file, done@\n"
let rec recompute_all_shapes_goal g =
......@@ -2337,25 +2337,27 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
loaded_provers = PHprover.create 5;
}
in
let obsolete = PHstr.fold (fun _ old_file acc ->
found_obsolete := false;
PHstr.iter (fun _ old_file ->
dprintf debug "[Load] file '%s'@\n" old_file.file_name;
let new_file = add_file
~keygen new_env_session
?format:old_file.file_format old_file.file_name
in
merge_file ~keygen new_env_session ~allow_obsolete old_file new_file