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

chore: leanmake: don't use CMake-like output by default

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-17 18:20:05 +02:00
parent 0f0f1407af
commit 52f2f04dff
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/lean.mk.in
View file

@ -49,7 +49,9 @@ $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
@deps=`lean --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
$(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Building $<"
endif
@mkdir -p $(OLEAN_OUT)/$(*D)
lean $(LEAN_OPTS) -o "$@" --c="$(TEMP_OUT)/$*.c.tmp" $<
# create the .c file atomically
@ -61,12 +63,16 @@ $(TEMP_OUT)/%.c: $(OLEAN_OUT)/%.olean
@
$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.c
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Building $<"
endif
@mkdir -p "$(@D)"
leanc -c -o $@ $< $(LEANC_OPTS)
$(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Linking $@"
endif
leanc -o "$@" -x none $^
$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)

3
src/stdlib.make.in
View file

@ -6,7 +6,8 @@ LEANMAKE_OPTS=\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
LEANC_OPTS="${LEANC_OPTS}"\
MORE_DEPS="${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}"
MORE_DEPS="${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}"\
CMAKE_LIKE_OUTPUT=1
stdlib:
ifeq "${STAGE}" "0.5"