max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: trying fix

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-29 13:37:38 -07:00
parent 3c476b4278
commit 57cdda5821
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/compiler/test_single_interpret.sh
View file

@ -25,21 +25,21 @@ if diff --color --help >/dev/null 2>&1; then
DIFF="diff --color";
fi
$LEAN --run "$ff" > "$ff.produced.out"
$LEAN --run "$ff" > "$ff.interp.produced.out"
if [ $? -ne 0 ]; then
echo "Failed to execute $ff"
exit 1
fi
if test -f "$ff.expected.out"; then
if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.interp.produced.out"; then
echo "-- checked"
exit 0
else
echo "ERROR: file $ff.produced.out does not match $ff.expected.out"
echo "ERROR: file $ff.interp.produced.out does not match $ff.expected.out"
if [ $INTERACTIVE == "yes" ]; then
meld "$ff.produced.out" "$ff.expected.out"
if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
meld "$ff.interp.produced.out" "$ff.expected.out"
if diff -I "executing external script" "$ff.expected.out" "$ff.interp.produced.out"; then
echo "-- mismatch was fixed"
fi
fi
@ -48,10 +48,10 @@ if test -f "$ff.expected.out"; then
else
echo "ERROR: file $ff.expected.out does not exist"
if [ $INTERACTIVE == "yes" ]; then
read -p "copy $ff.produced.out (y/n)? "
read -p "copy $ff.interp.produced.out (y/n)? "
if [ $REPLY == "y" ]; then
cp -- "$ff.produced.out" "$ff.expected.out"
echo "-- copied $ff.produced.out --> $ff.expected.out"
cp -- "$ff.interp.produced.out" "$ff.expected.out"
echo "-- copied $ff.interp.produced.out --> $ff.expected.out"
fi
fi
exit 1