sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

test: do not filter output for non-diff tests (#6308)

Browse Source
This commit is contained in:
Sebastian Ullrich
2024-12-04 18:49:35 +01:00
committed by GitHub
parent faf07e58db
commit 88573c802d
5 changed files with 25 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
doc/examples/test_single.sh
View File

@@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../tests/common.sh
exec_check lean -Dlinter.all=false "$f"
exec_check_raw lean -Dlinter.all=false "$f"

24
tests/common.sh
View File

@@ -39,17 +39,22 @@ function compile_lean_llvm_backend {
set +o xtrace
}
function exec_capture_raw {
# backtraces are system-specific, strip them (might be captured in `#guard_msgs`)
LEAN_BACKTRACE=0 "$@" 2>&1 > "$f.produced.out"
}
# produces filtered output intended for usage with `diff_produced`
function exec_capture {
# backtraces are system-specific, strip them
# mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' > "$f.produced.out"
}
# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.
function exec_check {
ret=0
function check_ret {
[ -n "${expected_ret+x}" ] || expected_ret=0
[ -f "$f.expected.ret" ] && expected_ret=$(< "$f.expected.ret")
exec_capture "$@" || ret=$?
if [ -n "$expected_ret" ] && [ $ret -ne $expected_ret ]; then
echo "Unexpected return code $ret executing '$@'; expected $expected_ret. Output:"
cat "$f.produced.out"
@@ -57,6 +62,19 @@ function exec_check {
fi
}
function exec_check_raw {
ret=0
exec_capture_raw "$@" || ret=$?
check_ret
}
# produces filtered output intended for usage with `diff_produced`
function exec_check {
ret=0
exec_capture "$@" || ret=$?
check_ret
}
function diff_produced {
if test -f "$f.expected.out"; then
if $DIFF -au --strip-trailing-cr -I "executing external script" "$f.expected.out" "$f.produced.out"; then

2
tests/lean/run/test_single.sh
View File

@@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../common.sh
exec_check lean -Dlinter.all=false "$f"
exec_check_raw lean -Dlinter.all=false "$f"

2
tests/lean/server/test_single.sh
View File

@@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../common.sh
exec_check lean -Dlinter.all=false --run "$f"
exec_check_raw lean -Dlinter.all=false --run "$f"

2
tests/lean/trust0/test_single.sh
View File

@@ -1,4 +1,4 @@
#!/usr/bin/env bash
source ../../common.sh
exec_check lean -t0 -Dlinter.all=false "$f"
exec_check_raw lean -t0 -Dlinter.all=false "$f"