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

feat(build): compile HoTT library when building

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-15 21:56:36 +01:00
parent 359bfe93d5
commit f7317a7139
4 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/Makefile.common
View file

@ -7,10 +7,10 @@ DEPS = make.deps
all: $(OLEAN_FILES) $(DEPS)
%.olean: %.lean
$(LEAN) $< -o $@
$(LEAN) $(LEAN_OPTIONS) $< -o $@
%.olean: %.lua
$(LEAN) $< -o $@
$(LEAN) $(LEAN_OPTIONS) $< -o $@
.PHONY: all clean

1
library/hott/Makefile Normal file
View file

@ -0,0 +1 @@
include ../Makefile.common

2
library/hott/logic.lean
View file

@ -139,7 +139,7 @@ inductive product (A : Type) (B : Type) : Type :=
infixr `∧`:30 := product
notation `(` h `,` t:(foldr `,` (e r, pair e r) h) `)` := t
notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t
definition pr1 {A : Type} {B : Type} (p : A ∧ B) : A
:= product_rec (λ a b, a) p

7
src/CMakeLists.txt
View file

@ -275,4 +275,11 @@ if((${CYGWIN} EQUAL "1") OR (NOT (${CMAKE_SYSTEM_NAME} MATCHES "Windows")))
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard
)
add_custom_target(
hott_lib ALL
COMMAND make LEAN="${CMAKE_BINARY_DIR}/shell/lean" LEAN_OPTIONS="--hott"
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/hott
)
endif()