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

feat(tests/lean/test_single): show unified diffs with color

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-05 12:59:38 +01:00
parent 98c2998a7b
commit 252931a470
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/test_single.sh
View file

@ -20,19 +20,24 @@ if [[ "$OSTYPE" == "msys" ]]; then
ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
fi
DIFF=diff
if diff --color --help >/dev/null 2>&1; then
DIFF="diff --color";
fi
echo "-- testing $f"
"$LEAN" -Dpp.colors=false -Dpp.unicode=true -j0 "$ff" &> "$f.produced.out"
sed 's|does\\not\\exist|does/not/exist|' "$f.produced.out" | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out.tmp"
mv "$f.produced.out.tmp" "$f.produced.out"
if test -f "$f.expected.out"; then
if diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"; then
if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
echo "-- checked"
exit 0
else
echo "ERROR: file $f.produced.out does not match $f.expected.out"
if [ $INTERACTIVE == "yes" ]; then
meld "$f.produced.out" "$f.expected.out"
if diff -I "executing external script" "$f.produced.out" "$f.expected.out"; then
if diff -I "executing external script" "$f.expected.out" "$f.produced.out"; then
echo "-- mismatch was fixed"
fi
fi