Commit 6ce9d548 authored by MARCHE Claude's avatar MARCHE Claude

fix file name used for editing. Better regtests script

parent 2c063df7
#!/bin/sh
# regression tests for why3
chdir `dirname $0`
cd `dirname $0`
TMP=/tmp/why3regtests.out
LOGIC="hello_proof scottish-private-club einstein"
SIMPLE="isqrt mac_carthy gcd gcd_bezout power"
FLOATS="my_cosine"
run_dir () {
for f in $2; do
echo -n "Replaying "$1/$f"... "
if ! why3replayer $1/$f 2>/dev/null > $TMP ; then
for f in `ls $1/*/why3session.xml`; do
d=`dirname $f`
echo -n "Replaying "$d"... "
if ! why3replayer $d 2>/dev/null > $TMP ; then
echo "FAILED:"
cat $TMP
# exit 1
......@@ -23,14 +20,11 @@ run_dir () {
}
echo "=== Logic ==="
run_dir . "$LOGIC"
run_dir .
echo ""
echo "=== Simple programs ==="
run_dir programs "$SIMPLE"
echo "=== Programs ==="
run_dir programs
echo ""
echo "=== Floating-point programs ==="
run_dir programs "$FLOATS"
echo ""
......@@ -530,7 +530,7 @@ let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
Driver.print_task ?old driver fmt goal;
Util.option_iter close_in old;
close_out ch;
let command = editor ^ " " ^ file in
let command = editor ^ " \"" ^ file ^ "\"" in
schedule_edition command callback
......
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