-
Notifications
You must be signed in to change notification settings - Fork 345
/
lean.mk.in
98 lines (79 loc) · 2.85 KB
/
lean.mk.in
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
# Copyright (c) 2018 Simon Hudon. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
# Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
# We compile all source files in $PKG/ as well as $PKG.lean. $PKG is also used for naming binary files.
ifndef PKG
PKG = $(strip $(subst .lean,, $(wildcard *.lean)))
ifneq ($(words $(PKG)), 1)
$(error no unique .lean file found in current directory, please specify PKG)
endif
endif
LEAN = lean
LEANC = leanc
OUT = build
OLEAN_OUT = $(OUT)
TEMP_OUT = $(OUT)/temp
BIN_OUT = $(OUT)/bin
LIB_OUT = $(OUT)/lib
BIN_NAME = $(PKG)
STATIC_LIB_NAME = lib$(PKG).a
LEAN_OPTS = @LEAN_EXTRA_MAKE_OPTS@
LEANC_OPTS = -O3 -DNDEBUG
LINK_OPTS =
SRCS = $(shell find $(PKG) -name '*.lean' 2> /dev/null || true; find $(PKG).lean 2> /dev/null)
DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend))
export LEAN_PATH += :$(OLEAN_OUT)
OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean))
SHELL = /usr/bin/env bash -eo pipefail
.PHONY: all bin lib depends clean
all: $(OBJS)
bin: $(BIN_OUT)/$(BIN_NAME)
lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
depends: $(DEPS)
$(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
@mkdir -p "$@"
# Make sure the .olean output directory exists so that `lean --deps` knows where this package's
# .olean files will be located even before any of them are actually built.
$(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
@mkdir -p "$(TEMP_OUT)/$(*D)"
# use separate assignment to ensure failure propagation
# convert path separators and newlines on Windows
@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
mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
# make sure the .olean file is newer than the .depend file to prevent infinite make cycles
@touch $@
$(TEMP_OUT)/%.c: $(OLEAN_OUT)/%.olean
@
$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.c
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Building $<"
endif
@mkdir -p "$(@D)"
ifdef PROFILE
\time -f "%U %S" leanc -c -o $@ $< $(LEANC_OPTS) 2>&1 > /dev/null | awk '{ printf "C compilation %fs\n", $$1 + $$2 }' > /dev/stderr
else
$(LEANC) -c -o $@ $< $(LEANC_OPTS)
endif
$(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
ifdef CMAKE_LIKE_OUTPUT
@echo "[ ] Linking $@"
endif
ifdef PROFILE
\time -f "%U %S" leanc -o "$@" -x none $^ $(LINK_OPTS) 2>&1 > /dev/null | awk '{ printf "C linking %fs\n", $$1 + $$2 }' > /dev/stderr
else
$(LEANC) -o "$@" -x none $^ $(LINK_OPTS)
endif
$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
@rm -f $@
@ar rcs $@ $^
clean:
rm -rf $(OUT)
.PRECIOUS: $(TEMP_OUT)/%.c
include $(DEPS)