Commit 4039cf04 authored by MARCHE Claude's avatar MARCHE Claude

diff in nightly bench

parent 0e1c37e4
#!/bin/bash
OUT=$PWD/nightly-bench.out
REPORT=$PWD/nightly-bench.report
REPORTDIR=$PWD/..
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
DATE=`date --utc +%Y-%m-%d`
notify() {
mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
......@@ -11,7 +15,7 @@ notify() {
}
echo "== Why3 bench on `date` ==" > $REPORT
echo "== Why3 bench on $DATE ==" > $REPORT
# configuration
autoconf
......@@ -20,7 +24,7 @@ if test "$?" != "0" ; then
echo "Configure failed" >> $REPORT
cat $OUT >> $REPORT
notify
else
else
echo "Configuration succeeded. " >> $REPORT
fi
......@@ -30,7 +34,7 @@ if test "$?" != "0" ; then
echo "Compilation failed" >> $REPORT
tail -20 $OUT >> $REPORT
notify
else
else
echo "Compilation succeeded. " >> $REPORT
fi
......@@ -40,7 +44,7 @@ if test "$?" != "0" ; then
echo "Prover detection failed" >> $REPORT
cat $OUT >> $REPORT
notify
else
else
echo "Prover detection succeeded. " >> $REPORT
fi
......@@ -52,10 +56,24 @@ perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why.conf
# replay proofs
examples/regtests.sh &> $OUT
if test "$?" != "0" ; then
cp $OUT $REPORTDIR/regtests-$DATE
echo "Proof replay failed" >> $REPORT
cat $OUT >> $REPORT
diff -u $PREVIOUS $OUT >> $DIFF
if test "$?" == 0 ; then
echo "---------- No difference with last bench ---------- " >> $REPORT
else
echo "" >> $REPORT
echo "--------------- Diff with last bench --------------" >> $REPORT
echo "" >> $REPORT
cp $OUT $PREVIOUS
sed '2d' $DIFF >> $REPORT
echo "" >> $REPORT
echo "-------------- Full current state --------------" >> $REPORT
echo "" >> $REPORT
cat $OUT >> $REPORT
fi
notify
else
else
echo "Replay succeeded. " >> $REPORT
fi
......
......@@ -35,17 +35,17 @@ echo "=== Logic ==="
run_dir .
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
# echo "=== BTS ==="
# run_dir bts
# echo ""
echo "=== Programs ==="
run_dir programs
echo ""
# echo "=== Programs ==="
# run_dir programs
# echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
# echo "=== Check Builtin translation ==="
# run_dir check-builtin
# echo ""
exit $res
......
......@@ -56,7 +56,7 @@ let fname = match !file with
let config = Whyconf.read_config None
let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
@ List.rev !includes
@ List.rev !includes
let env = Lexer.create_env loadpath
......@@ -158,7 +158,7 @@ let init =
| M.Goal g -> M.goal_expl g
| M.Theory th -> M.theory_name th
| M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a ->
| M.Proof_attempt a ->
begin
match a.M.prover with
| M.Detected_prover p ->
......@@ -170,6 +170,7 @@ let init =
(* eprintf "Item '%s' loaded@." name *)
()
(*
let string_of_result result =
match result with
| Session.Undone -> "undone"
......@@ -187,11 +188,19 @@ let string_of_result result =
let print_result fmt res =
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
Format.sprintf "(%.2f)" time
Format.sprintf "(%.1f)" time
| _ -> ""
in
fprintf fmt "%s%s" (string_of_result res) t
*)
let print_result fmt
{Call_provers.pr_answer=ans; Call_provers.pr_output=out;
Call_provers.pr_time=t} =
fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
if ans == Call_provers.HighFailure then
fprintf fmt "@\nProver output:@\n%s@." out
let notify _any = ()
(*
......@@ -247,33 +256,32 @@ let file_statistics (files,n,m) f =
((f,ths,n1,m1)::files,n+n1,m+m1)
let print_statistics files =
List.iter
List.iter
(fun (f,ths,n,m) ->
if n<m then
begin
printf " +--file %s: %d/%d@." f.M.file_name n m;
List.iter
List.iter
(fun (th,goals,n,m) ->
if n<m then
begin
printf " +--theory %s: %d/%d@."
printf " +--theory %s: %d/%d@."
(M.theory_name th) n m;
List.iter
List.iter
(fun g ->
printf " +--goal %s not proved@." (M.goal_name g))
printf " +--goal %s not proved@." (M.goal_name g))
(List.rev goals)
end)
(List.rev ths)
end)
(List.rev files)
let print_report (g,p,r) =
let print_report (g,p,r) =
printf " goal '%s', prover '%s': " g p;
match r with
| M.Wrong_result(new_res,old_res) ->
| M.Wrong_result(new_res,old_res) ->
printf "%a instead of %a@."
Call_provers.print_prover_result new_res
Call_provers.print_prover_result old_res
print_result new_res print_result old_res
| M.No_former_result ->
printf "no former result available@."
| M.CallFailed msg ->
......@@ -281,8 +289,6 @@ let print_report (g,p,r) =
| M.Prover_not_installed ->
printf "not installed@."
let () =
try
eprintf "Opening session...@?";
......@@ -291,19 +297,19 @@ let () =
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
let callback report =
let files,n,m =
List.fold_left file_statistics ([],0,0) (M.get_all_files ())
let files,n,m =
List.fold_left file_statistics ([],0,0) (M.get_all_files ())
in
printf " %d/%d@." n m ;
match report with
| [] ->
| [] ->
if !opt_stats && n<m then print_statistics files;
eprintf "Everything OK.@.";
exit 0
| _ ->
List.iter print_report report;
eprintf "Check failed.@.";
exit 1
eprintf "Check failed.@.";
exit 1
in
M.check_all ~callback;
try main_loop ()
......
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