Commit 4eacde07 authored by MARCHE Claude's avatar MARCHE Claude

Relativized path names of edited proofs

Allows to replay Coq proofs correctly
There is still a problem with goal names containing spaces such as
those generated by VC generator
parent 41badd75
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="power/why3session.xml">
<why3session name="examples/programs/power/why3session.xml">
<file name="../power.mlw" verified="false" expanded="true">
<theory name="Power" verified="true" expanded="false">
<theory name="Power" verified="true" expanded="true">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
......@@ -17,8 +17,8 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power/power.mlw_Power_Power_sum_1.v" obsolete="false">
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.46"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
......@@ -35,7 +35,7 @@
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="false">
<proof prover="coq" timelimit="2" edited="power/power.mlw_Power_Power_mult_1.v" obsolete="false">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
......
#!/bin/sh
# regression tests for why3
chdir `dirname $0`
TMP=/tmp/why3regtests.out
LOGIC="hello_proof scottish-private-club einstein"
......
......@@ -238,7 +238,7 @@ let main () =
in
M.check_all ~callback;
try main_loop ()
with Exit -> eprintf "Everything done@."
with Exit -> eprintf "main replayer exited unexpectedly@."
with e ->
eprintf "Error while opening session with database '%s'@." project_dir;
eprintf "Aborting...@.";
......
......@@ -1199,8 +1199,9 @@ let redo_external_proof ~timelimit g a =
in
let old = if a.edited_as = "" then None else
begin
Format.eprintf "Info: proving using edited file %s@." a.edited_as;
(Some (open_in a.edited_as))
let f = Filename.concat !project_dir a.edited_as in
Format.eprintf "Info: proving using edited file %s@." f;
(Some (open_in f))
end
in
schedule_proof_attempt
......@@ -1358,8 +1359,9 @@ let check_external_proof g a =
in
let old = if a.edited_as = "" then None else
begin
(* Format.eprintf "Info: proving using edited file %s@." a.edited_as; *)
(Some (open_in a.edited_as))
let f = Filename.concat !project_dir a.edited_as in
(* Format.eprintf "Info: proving using edited file %s@." f; *)
(Some (open_in f))
end
in
incr proofs_to_do;
......@@ -1390,6 +1392,7 @@ let check_all ~callback =
Printf.eprintf "Progress: %d/%d\r%!" !proofs_done !proofs_to_do;
if !proofs_done = !proofs_to_do then
begin
Printf.eprintf "\n%!";
callback !check_failed;
false
end
......@@ -1542,10 +1545,12 @@ let edit_proof ~default_editor ~project_dir a =
incr i
done;
let file = name ^ "_" ^ (string_of_int !i) ^ ext in
let file = Sysutil.relativize_filename project_dir file in
a.edited_as <- file;
file
| f -> f
in
let file = Filename.concat project_dir file in
let callback res =
match res with
| Done _ ->
......@@ -1558,6 +1563,10 @@ let edit_proof ~default_editor ~project_dir a =
| "" -> default_editor
| s -> s
in
(*
eprintf "[Editing] goal %s with command %s %s@." g.Decl.pr_name.id_string editor file;
*)
eprintf "[Editing] goal %s with command %s %s@." (Task.task_goal t).Decl.pr_name.Ident.id_string editor file;
schedule_edit_proof ~debug:false ~editor
~file
~driver
......
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