feat(tests/lean): include standard error in the expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e0eeb7c8d5
commit
6b1b6c7bd1
6 changed files with 29 additions and 2 deletions
|
@ -4,3 +4,8 @@
|
||||||
Assumed: g
|
Assumed: g
|
||||||
Assumed: p
|
Assumed: p
|
||||||
Assumed: h
|
Assumed: h
|
||||||
|
The denotation(s) for the existing notation:
|
||||||
|
Infix ++
|
||||||
|
have been replaced with the new denotation:
|
||||||
|
h::explicit
|
||||||
|
because they conflict on how implicit arguments are used.
|
||||||
|
|
|
@ -5,3 +5,8 @@
|
||||||
Assumed: h
|
Assumed: h
|
||||||
Assumed: p
|
Assumed: p
|
||||||
Assumed: p2
|
Assumed: p2
|
||||||
|
The denotation(s) for the existing notation:
|
||||||
|
Infix ++
|
||||||
|
have been replaced with the new denotation:
|
||||||
|
p2::explicit
|
||||||
|
because they conflict on how implicit arguments are used.
|
||||||
|
|
|
@ -3,9 +3,11 @@
|
||||||
Importing file 'simple.lean'
|
Importing file 'simple.lean'
|
||||||
Assumed: x
|
Assumed: x
|
||||||
Assumed: y
|
Assumed: y
|
||||||
|
Module 'simple.lean' has already been imported
|
||||||
Importing file 'simple.lean'
|
Importing file 'simple.lean'
|
||||||
Assumed: x
|
Assumed: x
|
||||||
Assumed: y
|
Assumed: y
|
||||||
|
Module 'simple.lean' has already been imported
|
||||||
x + y : ℤ
|
x + y : ℤ
|
||||||
Assumed: z
|
Assumed: z
|
||||||
z : ℤ
|
z : ℤ
|
||||||
|
|
|
@ -1,4 +1,19 @@
|
||||||
Set: pp::colors
|
Set: pp::colors
|
||||||
Set: pp::unicode
|
Set: pp::unicode
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
|
||||||
Proved: T
|
Proved: T
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
|
||||||
|
Proof state:
|
||||||
|
H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
|
||||||
Proved: T2
|
Proved: T2
|
||||||
|
|
|
@ -13,7 +13,7 @@ fi
|
||||||
NUM_ERRORS=0
|
NUM_ERRORS=0
|
||||||
for f in `ls *.lean`; do
|
for f in `ls *.lean`; do
|
||||||
echo "-- testing $f"
|
echo "-- testing $f"
|
||||||
$LEAN config.lean $f > $f.produced.out
|
$LEAN config.lean $f &> $f.produced.out
|
||||||
if test -f $f.expected.out; then
|
if test -f $f.expected.out; then
|
||||||
if diff $f.produced.out $f.expected.out; then
|
if diff $f.produced.out $f.expected.out; then
|
||||||
echo "-- checked"
|
echo "-- checked"
|
||||||
|
|
|
@ -12,7 +12,7 @@ else
|
||||||
fi
|
fi
|
||||||
f=$2
|
f=$2
|
||||||
echo "-- testing $f"
|
echo "-- testing $f"
|
||||||
$LEAN config.lean $f > $f.produced.out
|
$LEAN config.lean $f &> $f.produced.out
|
||||||
if test -f $f.expected.out; then
|
if test -f $f.expected.out; then
|
||||||
if diff $f.produced.out $f.expected.out; then
|
if diff $f.produced.out $f.expected.out; then
|
||||||
echo "-- checked"
|
echo "-- checked"
|
||||||
|
|
Loading…
Reference in a new issue