michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(tests/lean/interactive): add interactive mode test script

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-05 16:56:20 -08:00
parent e3848d43a2
commit 34654ad06b
8 changed files with 164 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/parser.cpp
View file

@ -1255,7 +1255,7 @@ class parser::imp {
return;
}
}
throw tactic_cmd_error("no more states to backtrack", p, s);
throw tactic_cmd_error("failed to backtrack", p, s);
}
void tactic_apply(proof_state_seq_stack & stack, proof_state & s) {
@ -1308,7 +1308,7 @@ class parser::imp {
}
return pr;
} else {
throw tactic_cmd_error("failed to synthesize proof object using tactics", p, s);
throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s);
}
}
@ -1356,11 +1356,12 @@ class parser::imp {
} else if (id == g_back) {
tactic_backtrack(stack, s);
} else if (id == g_done) {
done = true;
pr = tactic_done(s);
if (pr)
done = true;
} else {
next();
throw tactic_cmd_error(sstream() << "invalid tactical proof, unknown command '" << id << "'", p, s);
throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
}
break;
default:

18
src/shell/CMakeLists.txt
View file

@ -8,7 +8,7 @@ add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../exampl
add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean")
add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
# LEANTESTS
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
FOREACH(T ${LEANTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -17,7 +17,16 @@ FOREACH(T ${LEANTESTS})
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
ENDFOREACH(T)
# LEANSLOWTESTS
# LEAN INTERACTIVE TESTS
file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
FOREACH(T ${LEANINTERACTIVETESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leaninteractivetest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
ENDFOREACH(T)
# LEAN SLOW TESTS
file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
FOREACH(T ${LEANSLOWTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -26,7 +35,7 @@ FOREACH(T ${LEANSLOWTESTS})
COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
ENDFOREACH(T)
# LEANLUATESTS
# LEAN LUA TESTS
file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
FOREACH(T ${LEANLUATESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -35,7 +44,7 @@ FOREACH(T ${LEANLUATESTS})
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
ENDFOREACH(T)
# LEANLUADOCS
# LEAN LUA DOCS
file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md")
FOREACH(T ${LEANLUADOCS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -44,6 +53,7 @@ FOREACH(T ${LEANLUADOCS})
COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
ENDFOREACH(T)
# LEAN LUA THREAD TESTS
if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${THREAD_SAFE} MATCHES "ON"))
file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua")

3
tests/lean/interactive/config.lean Normal file
View file

@ -0,0 +1,3 @@
(* Set default configuration for tests *)
Set pp::colors false
Set pp::unicode true

5
tests/lean/interactive/config.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Set: pp::colors
Set: pp::unicode

12
tests/lean/interactive/t1.lean Normal file
View file

@ -0,0 +1,12 @@
Theorem T2 (a b : Bool) : a => b => a /\ b.
done.
done.
apply imp_tactic.
apply imp_tactic2.
foo.
apply imp_tactic.
apply imp_tactic.
apply conj_tactic.
back.
apply assumption_tactic.
done.

35
tests/lean/interactive/t1.lean.expected.out Normal file
View file

@ -0,0 +1,35 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proof state:
a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
## Error (line: 5, pos: 0) invalid 'done' command, proof cannot be produced from this state
Proof state:
a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
## Error (line: 6, pos: 0) invalid 'done' command, proof cannot be produced from this state
Proof state:
a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
## Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Error (line: 8, pos: 0) unknown tactic 'imp_tactic2'
Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Error (line: 9, pos: 0) invalid tactic command 'foo'
Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
## Error (line: 11, pos: 0) tactic failed
Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a
H::1 : b, H : a, a : Bool, b : Bool ⊢ b
## Error (line: 13, pos: 0) failed to backtrack
Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a
H::1 : b, H : a, a : Bool, b : Bool ⊢ b
## Proof state:
no goals
## Proved: T2
#

48
tests/lean/interactive/test.sh Executable file
View file

@ -0,0 +1,48 @@
#!/bin/bash
if [ $# -ne 2 -a $# -ne 1 ]; then
echo "Usage: test.sh [lean-executable-path] [yes/no]?"
exit 1
fi
ulimit -s unlimited
LEAN=$1
if [ $# -ne 2 ]; then
INTERACTIVE=no
else
INTERACTIVE=$2
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
if test -f $f.expected.out; then
if diff $f.produced.out $f.expected.out; then
echo "-- checked"
else
echo "ERROR: file $f.produced.out does not match $f.expected.out"
NUM_ERRORS=$(($NUM_ERRORS+1))
if [ $INTERACTIVE == "yes" ]; then
meld $f.produced.out $f.expected.out
if diff $f.produced.out $f.expected.out; then
echo "-- mismath was fixed"
fi
fi
fi
else
echo "ERROR: file $f.expected.out does not exist"
NUM_ERRORS=$(($NUM_ERRORS+1))
if [ $INTERACTIVE == "yes" ]; then
read -p "copy $f.produced.out (y/n)? "
if [ $REPLY == "y" ]; then
cp $f.produced.out $f.expected.out
echo "-- copied $f.produced.out --> $f.expected.out"
fi
fi
fi
done
if [ $NUM_ERRORS -gt 0 ]; then
echo "-- Number of errors: $NUM_ERRORS"
exit 1
else
echo "-- Passed"
exit 0
fi

42
tests/lean/interactive/test_single.sh Executable file
View file

@ -0,0 +1,42 @@
#!/bin/bash
if [ $# -ne 3 -a $# -ne 2 ]; then
echo "Usage: test.sh [lean-executable-path] [file] [yes/no]?"
exit 1
fi
ulimit -s unlimited
LEAN=$1
if [ $# -ne 3 ]; then
INTERACTIVE=no
else
INTERACTIVE=$3
fi
f=$2
echo "-- testing $f"
cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
if test -f $f.expected.out; then
if diff $f.produced.out $f.expected.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 $f.produced.out $f.expected.out; then
echo "-- mismath was fixed"
fi
else
diff $f.produced.out $f.expected.out
fi
exit 1
fi
else
echo "ERROR: file $f.expected.out does not exist"
if [ $INTERACTIVE == "yes" ]; then
read -p "copy $f.produced.out (y/n)? "
if [ $REPLY == "y" ]; then
cp $f.produced.out $f.expected.out
echo "-- copied $f.produced.out --> $f.expected.out"
fi
fi
exit 1
fi