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

feat(builtin): remove lean executable as a dependency for builtin .lean files

Browse source 
Otherwise, we have to rebuild all .lean files whenever we change the executable.
This commit also adds a test for each .lean file.
This is useful for increasing coverage and having a log on how long does it take to process these files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-07 13:52:55 -08:00
parent 4523a9f22a
commit 6077dc61b7
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/builtin/CMakeLists.txt
View file

@ -30,10 +30,11 @@ function(add_theory_core FILE ARG EXTRA_DEPS)
COMMAND ${SHELL_DIR}/lean ${ARG} -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME}
COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME}
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS})
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${EXTRA_DEPS})
add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS})
add_dependencies(builtin ${BASENAME}_builtin)
install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library)
add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE})
endfunction()
# When cross compiling, we cannot execute lean during the build.
@ -73,3 +74,5 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")
add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean")