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

chore: add doc/examples to the test suite

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-24 15:20:18 -07:00
parent 53faa9c8ca
commit 52a52fbed7
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/examples/test_single.sh Executable file
View file

@ -0,0 +1,4 @@
#!/usr/bin/env bash
source ../../tests/common.sh
exec_check lean -j 0 "$f"

11
src/shell/CMakeLists.txt
View file

@ -71,6 +71,17 @@ FOREACH(T ${LEANRUNTESTS})
endif()
ENDFOREACH(T)
# LEAN RUN doc/examples
file(GLOB LEANDOCEXS "${LEAN_SOURCE_DIR}/../doc/examples/*.lean")
FOREACH(T ${LEANDOCEXS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leandocex_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
endif()
ENDFOREACH(T)
# LEAN COMPILER TESTS
file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
FOREACH(T ${LEANCOMPTESTS})