-
Notifications
You must be signed in to change notification settings - Fork 1
/
Makefile.common
221 lines (181 loc) · 7.76 KB
/
Makefile.common
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # Copyright INRIA, CNRS and contributors ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
-include config/Makefile
###########################################################################
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.
# Quiet mode is ON by default except if VERBOSE=1 option is given to make
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
###########################################################################
# Basic build directories
###########################################################################
BCONTEXT=_build/default
CONTEXT=_build/install/default
CBIN=_build/install/default/bin
CSHARE=_build/install/default/share/coq
_DBUILD_DEPS:=
# FLOCK
ifeq (,$(shell command -v flock 2>/dev/null))
FLOCK:=_build/default/tools/flock/coq_flock.exe
_DBUILD_DEPS+=$(FLOCK)
$(FLOCK): tools/flock/coq_flock.ml tools/flock/flock.c
$(SHOW)'DUNE $@'
$(HIDE)dune build $@
else
FLOCK:=flock
endif
# Standard DESTDIR variable as used in Debian and coq_makefile, will
# have make install prefixing all install targets with DESTDIR
DESTDIR ?=
###########################################################################
# VO build directory
###########################################################################
# slash at the end allows us to define this variable as empty, be
# careful, the slash is mandatory.
#
# Note, we can use this as _build/default , but unfortunately dune
# will remove the .vos files as they are not recognized as targets
BUILD_OUT_DIR=_build_vo/default/
VO_OUT_DIR=$(BUILD_OUT_DIR)/lib/coq/
LEGACY_BIN_DIR=bin
$(BUILD_OUT_DIR) $(VO_OUT_DIR):
$(SHOW)'MKDIR BUILD_OUT'
$(HIDE)mkdir -p $(BUILD_OUT_DIR)
$(HIDE)mkdir -p $(BUILD_OUT_DIR)/lib/coq
$(HIDE)mkdir -p $(BUILD_OUT_DIR)/lib/coq-core
$(HIDE)ln -s $(shell pwd)/_build/install/default/bin/ $(LEGACY_BIN_DIR)
$(HIDE)ln -s $(shell pwd)/_build/install/default/bin/ $(BUILD_OUT_DIR)/bin
$(HIDE)ln -s $(shell pwd)/_build/default/plugins/ $(BUILD_OUT_DIR)/lib/coq-core
$(HIDE)ln -s $(shell pwd)/_build/default/tools/ $(BUILD_OUT_DIR)/lib/coq-core
$(HIDE)ln -s $(shell pwd)/_build/default/kernel/ $(BUILD_OUT_DIR)/lib/coq-core
###########################################################################
# Executables
###########################################################################
ifeq ($(BEST),byte)
COQC:=$(CBIN)/coqc.byte$(EXE)
export CAML_LD_LIBRARY_PATH:=$(shell echo $(CONTEXT)/lib/stublibs:$$CAML_LD_LIBRARY_PATH)
else
COQC:=$(CBIN)/coqc$(EXE)
endif
COQTOPEXE:=$(CBIN)/coqtop$(EXE)
TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix $(CBIN)/, coqproofworker coqtacticworker coqqueryworker)) $(COQTOPEXE)
COQDEP:=$(CBIN)/coqdep$(EXE)
DOC_GRAM:=_build/default/doc/tools/docgram/doc_grammar.exe
COQMAKEFILE:=$(CBIN)/coq_makefile$(EXE)
COQMAKEFILEIN:=$(BCONTEXT)/tools/CoqMakefile.in
COQTEX:=$(CBIN)/coq-tex$(EXE)
COQWC:=$(CBIN)/coqwc$(EXE)
COQDOC:=$(CBIN)/coqdoc$(EXE)
COQNATIVE:=$(CBIN)/coqnative$(EXE)
COQDOCSTY:=$(CONTEXT)/lib/coq-core/tools/coqdoc/coqdoc.sty
COQDOCCSS:=$(CONTEXT)/lib/coq-core/tools/coqdoc/coqdoc.css
COQWORKMGR:=$(CBIN)/coqworkmgr$(EXE)
COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
VOTOUR:=$(CBIN)/votour$(EXE)
OCAMLLIBDEP:=$(CBIN)/ocamllibdep$(EXE)
USERCONTRIBDIRS:=Ltac2
CHICKEN:=$(CBIN)/coqchk$(EXE)
TOOLS:=$(VOTOUR) $(COQDOC) $(COQDOCSTY) $(COQDOCCSS) $(COQWC) $(COQMAKEFILE) $(COQMAKEFILEIN) $(COQNATIVE)
CSDPCERT:=$(CBIN)/csdpcert$(EXE)
ifeq ($(origin COQ_SRC_DIR),undefined)
COQ_SRC_DIR=.
endif
COQ_CM_LIBS=coqpp lib clib kernel library engine pretyping gramlib interp printing parsing proofs tactics vernac stm toplevel topbin tools
ML_SOURCE_DIRS=$(addprefix $(COQ_SRC_DIR)/,$(COQ_CM_LIBS))
ALL_ML_SOURCE_FILES=$(shell find $(ML_SOURCE_DIRS) -name '*.ml' -or -name '*.mli' -or -name '*.c' -or -name '*.h')
DOCGRAM_SOURCE_FILES=$(shell find $(addprefix $(COQ_SRC_DIR)/, doc/tools/docgram) -name '*.ml' -or -name '*.mlg')
# Override for developer build [to get warn-as-error for example]
_DDISPLAY?=quiet
_DPROFILE?=$(CONFIGURE_DPROFILE)
_DOPT:=--display=$(_DDISPLAY) $(_DPROFILE)
_DBUILD:=$(FLOCK) .dune.lock dune build $(_DOPT)
# We rerun dune when any of the source files have changed
# touch is needed for all targets in `_build` as make won't track
# symlink's date correctly [and dune won't update the mtime as it
# doesn't use it as the main criteria], so if we didn't touch an
# updated mtime in a source file may not trigger a dune rebuild it it
# didn't change hash, thus the mtime of the target would confuse make.
$(CBIN)/%: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
$(CSHARE)/%: $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
ALL_PLUGIN_SOURCE_FILES=$(shell find $(COQ_SRC_DIR)/plugins -name '*.ml' -or -name '*.mli' -or -name '*.mlg') $(ALL_ML_SOURCE_FILES)
_build/default/plugins/%.cmxs: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/default/plugins/%.cma: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
# Only used for the test-suite in local mode
_build/default/tools/%: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/install/default/lib/coq-core/plugins/%.cmxs: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/install/default/lib/stublibs/%.so: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/install/default/lib/coq/%.cmi: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty: $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css: $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/default/%.install: $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
ALL_CONTRIB_SOURCE_FILES=$(shell find $(COQ_SRC_DIR)/user-contrib -name '*.ml' -or -name '*.mli' -or -name '*.mlg') $(ALL_PLUGIN_SOURCE_FILES)
_build/default/user-contrib/%.cmxs: $(ALL_CONTRIB_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
_build/default/user-contrib/%.cma: $(ALL_CONTRIB_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
.PHONY: all-src
ALL_SOURCE_FILES=$(ALL_CONTRIB_SOURCE_FILES) $(ALL_PLUGIN_SOURCE_FILES) $(ALL_ML_SOURCE_FILES)
all-src: $(ALL_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE sources'
$(HIDE)$(_DBUILD) @all-src
# For docgram
_build/default/doc/tools/%: $(ALL_ML_SOURCE_FILES) $(DOCGRAM_SOURCE_FILES) $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
PLUGINTUTO := doc/plugin_tutorial
revision: $(_DBUILD_DEPS)
$(SHOW)'DUNE $@'
$(HIDE)$(_DBUILD) $@
$(HIDE)touch $@
# For emacs:
# Local Variables:
# mode: makefile
# End: