feat(build): add HoTT library to build
This commit is contained in:
parent
eb87c18693
commit
0034ad9b34
2 changed files with 7 additions and 1 deletions
|
@ -506,7 +506,7 @@ def find_lean_files(args):
|
|||
files -= set(find_files(project_dir, pattern))
|
||||
has_lean = False
|
||||
has_hlean = False
|
||||
for file in args.targets:
|
||||
for file in files:
|
||||
if file.endswith(".lean"):
|
||||
has_lean = True
|
||||
if file.endswith(".hlean"):
|
||||
|
|
|
@ -373,6 +373,12 @@ else()
|
|||
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
|
||||
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library
|
||||
)
|
||||
add_custom_target(
|
||||
hott_lib ALL
|
||||
COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja all tags
|
||||
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
|
||||
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../hott
|
||||
)
|
||||
endif()
|
||||
|
||||
add_custom_target(clean-olean
|
||||
|
|
Loading…
Reference in a new issue