fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
caea19dcf0
commit
a75d05fdb4
16 changed files with 2 additions and 16 deletions
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Set: pp::colors
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proved: T1
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proved: T1
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Error (line: 4, pos: 8) invalid definition, identifier expected
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Assumed: magic
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Assumed: q
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Set: tactic::proof_state::goal_names
|
||||
|
|
|
@ -1,4 +1,3 @@
|
|||
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
|
||||
# Set: pp::colors
|
||||
Set: pp::unicode
|
||||
Proof state:
|
||||
|
|
|
@ -13,7 +13,7 @@ fi
|
|||
NUM_ERRORS=0
|
||||
for f in `ls *.lean`; do
|
||||
echo "-- testing $f"
|
||||
cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
|
||||
cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out
|
||||
if test -f $f.expected.out; then
|
||||
if diff $f.produced.out $f.expected.out; then
|
||||
echo "-- checked"
|
||||
|
|
|
@ -12,7 +12,7 @@ else
|
|||
fi
|
||||
f=$2
|
||||
echo "-- testing $f"
|
||||
cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
|
||||
cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out
|
||||
if test -f $f.expected.out; then
|
||||
if diff $f.produced.out $f.expected.out; then
|
||||
echo "-- checked"
|
||||
|
|
Loading…
Reference in a new issue