This repository has been archived by the owner on Nov 7, 2020. It is now read-only.
forked from jyh/metaprl
-
Notifications
You must be signed in to change notification settings - Fork 1
/
OMakefile_common
374 lines (316 loc) · 10.6 KB
/
OMakefile_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
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
#
# Make sure omake is up-to-date
#
OMakeVersion(0.9.8.5)
########################################################################
# Config cleaning
#
if $(not $(defined CAMLP5R))
CAMLP5R = camlp5r$(EXE)
export
if $(not $(defined CAMLP5O))
CAMLP5O = camlp5o$(EXE)
export
#
# Inline more aggressively
#
if $(not $(NATIVE_PROFILING_ENABLED))
OCAMLOPTFLAGS += -inline $(OCAMLOPT_INLINE)
export
#
# Do not compile MetaPRL with threads.
#
THREADSLIB[] =
OPTTHREADSLIB[] =
OCAML_OTHER_LIBS += unix
if $(THREADS_ENABLED)
OCAMLFLAGS += -thread
OCAML_OTHER_LIBS += threads
THREADSLIB = $(CAMLLIB)/threads/threads.cma
OPTTHREADSLIB = $(CAMLLIB)/threads/threads.cmxa
export
#
# For native code profiling, we need both versions of the filter libraries.
#
if $(NATIVE_PROFILING_ENABLED)
COMPILATION_MODE = both
OCAMLOPTFLAGS += -p -inline 0
CFLAGS += -p -DPROF
if $(equal $(NATIVE_PROFILING_ENABLED), compact)
OCAMLOPTFLAGS += -compact
export
export
########################################################################
# Version and config checking
#
CheckVar(name, val, valid) =
if $(not $(mem $(val), $(valid)))
valid = $(array $(valid))
valid = $(concat $', ', $(valid.map $(quote)))
err[] =
$"""The $(name) variable is currently set to an invalid value "$(val)"."""
$"""Valid values for $(name) are: $(valid)."""
$"""Please fix it in the mk/config file."""
ConfMsgError($(err))
CheckVar(COMPILATION_MODE, $(COMPILATION_MODE), native byte mixed both)
NATIVE_ENABLED = $(mem $(COMPILATION_MODE), native mixed both)
BYTE_ENABLED = $(mem $(COMPILATION_MODE), byte mixed both)
CheckFile(f, err-extra) =
f = $(file $"$f")
if $(not $(file-exists $f))
err[] =
$"The file $f does not exist (or is not readable)"
$(EMPTY)
$(err-extra)
ConfMsgError($(err))
InstVarErr(var) =
err[] =
$"Please consult doc/htmlman/mp-install.html (http://metaprl.org/install.html)"
$"for instructions on compiling OCaml and setting the $(var) variable."
return $(err)
if $(file-exists $(CAMLLIB)/../compiler-lib/parsetree.cmi)
OCAMLINCLUDES += $(dir $(CAMLLIB)/../compiler-lib)
export
elseif $(file-exists $(CAMLLIB)/compiler-libs/parsetree.cmi)
OCAMLINCLUDES += $(dir $(CAMLLIB)/compiler-libs)
export
else
if $(BYTE_ENABLED)
CheckFile($(CAMLLIB)/parsetree.cmi, $(InstVarErr CAMLLIB))
if $(BYTE_ENABLED)
CheckFile($(CAMLP5LIB)/camlp5.cma, $(InstVarErr CAMLP5LIB))
CheckFile($(CAMLP5LIB)/pa_op.cmo, $(InstVarErr CAMLP5LIB))
if $(NATIVE_ENABLED)
CheckFile($(CAMLP5LIB)/camlp5.cmxa, $(InstVarErr CAMLP5LIB))
CheckFile($(CAMLP5LIB)/pa_op.cmx, $(InstVarErr CAMLP5LIB))
CheckVar(TERMS, $(TERMS), std ds both)
CheckVar(REFINER, $(REFINER), SIMPLE VERBOSE)
CheckVar(SEQ_SET, $(SEQ_SET), Lm_array Lm_splay)
CheckVar(DEFAULT_UI, $(DEFAULT_UI), browser cli)
if $(equal $(OSTYPE), Win32)
if $(SSL_ENABLED)
err[] =
$"Please either"
$" - Make sure your OpenSSL installation is complete and"
$" the SSL_LIB_WIN32 and SSL_INC_WIN32 variables in mk/config.local"
$" point to the correct location"
$" - Set SSL_ENABLED to false in mk/config"
$" Note that SSL is currently required for the browser interface to work"
CheckFile($(SSL_LIB_WIN32)/ssleay32MT.lib, $(err))
CheckFile($(SSL_LIB_WIN32)/libeay32MT.lib, $(err))
CheckFile($(SSL_INC_WIN32)/openssl/ssl.h, $(err))
#
# Different version files
#
OCAMLC_VERSION = $(file .version.ocamlc)
OCAMLOPT_VERSION = $(file .version.ocamlopt)
CAMLP5_VERSION = $(file .version.camlp5)
CAMLP5R_VERSION = $(file .version.camlp5r)
CAMLP5O_VERSION = $(file .version.camlp5o)
OCAMLMKTOP_VERSION = $(file .version.ocamlmktop)
#
# Generate the rule for version checking.
#
VersionCheck(versionfile, command, ?opt = -version) =
fullcommand = $(which $(command))
$(versionfile): $(fullcommand)
section eval
tmpname = $(tmpfile version)
$(command) $(opt) >& $(tmpname)
version = $(cat $(tmpname))
match $(version)
case $".*version.\([.0-9]+\).*"
version = $1
export
if $(mem $(version), $(CAML_VERSIONS))
fd = $(fopen $(versionfile), w)
fprintln($(fd), $(version))
close($(fd))
else
if $(SHARED_MODE)
err[] =
$"Wrong CAML version: $(version)"
$(EMPTY)
Your MetaPRL installation in $(MP_ROOT)
was compiled using OCaml version $(CAML_VERSIONS)
You have to use the same version of OCaml for your own theories.
ConfMsgError($(err))
else
err[] =
$"Unsupported CAML version: $(version)"
$(EMPTY)
$"""$(EMPTY)"$(command) $(opt)" produced the version string "$(version)"$(EMPTY)"""
$"You need this version to be compatible with MetaPRL,"
$"which is only known to work with versions $(CAML_VERSIONS)"
$(EMPTY)
$"If you believe that this list of versions is incorrect, edit"
$"the CAML_VERSIONS variable in the mk/defaults file."
ConfMsgError($(err))
VersionCheck($(OCAMLC_VERSION), $(OCAMLC))
VersionCheck($(OCAMLOPT_VERSION), $(OCAMLOPT))
VersionCheck($(OCAMLMKTOP_VERSION), $(OCAMLMKTOP))
section
CAML_VERSIONS = $(CAMLP5_VERSIONS)
VersionCheck($(CAMLP5_VERSION), $(CAMLP5), ?opt = $"-version")
VersionCheck($(CAMLP5R_VERSION), $(CAMLP5R), ?opt = $"-version")
VersionCheck($(CAMLP5O_VERSION), $(CAMLP5O), ?opt = $"-version")
#
# XXX: This is here to make sure that Camlp5 3.08 acts the same way as 3.09
# (in 3.08 the default value is loc, but in 3.09 it's _loc).
#
LOC = -loc _loc
%.cmo %.cmi: $(OCAMLC_VERSION)
%.cmx: $(OCAMLOPT_VERSION)
########################################################################
# Installation into $(LIB) and $(BIN)
#
#
# Copy into the $(BIN) directory
#
BinInstall(files) =
foreach(src => ..., $(files))
$(BIN)/$(src): $(src) $(BIN)
ln-or-cp $< $@
$(MPINSTALL): $(addprefix $(BIN)/, $(files))
#
# Install into the $(LIB) directory.
#
LibInstallDir(subdir) =
$(LIB)/$(subdir):
mkdir -p $@
LibSubInstallNamed(subdir, dst, src) =
$(LIB)/$(subdir)/$(dst): $(src) $(LIB)/$(subdir) :scanner: $(NOSCANNER)
ln-or-cp $< $@
$(MPINSTALL): $(LIB)/$(subdir)/$(dst)
LibSubInstall(subdir, files) =
foreach(src => ..., $(files))
LibSubInstallNamed($(subdir), $(basename $(src)), $(src))
LibInstall(files) =
LibSubInstall($(EMPTY), $(files))
#
# Install into the $(EXPORT) directory.
#
ExportInstallDir(subdir) =
$(EXPORT)/$(subdir):
mkdir -p $@
ExportSubInstallNamed(subdir, dst, src) =
$(EXPORT)/$(subdir)/$(dst): $(src) $(EXPORT)/$(subdir) :scanner: $(NOSCANNER)
ln-or-cp $< $@
$(MPINSTALL): $(EXPORT)/$(subdir)/$(dst)
ExportSubInstall(subdir, files) =
foreach(src => ..., $(files))
ExportSubInstallNamed($(subdir), $(basename $(src)), $(src))
ExportInstall(files) =
ExportSubInstall($(EMPTY), $(files))
########################################################################
# MetaPRL-specific config cleaning
#
#
# Library suffix
#
if $(NATIVE_ENABLED)
LIB_SUFFIX = .cmxa
OBJ_SUFFIX = .opt
export
else
LIB_SUFFIX = .cma
OBJ_SUFFIX = .top
export
#
# Whether to compile a distributed version or not
#
if $(equal $(ENSROOT), undefined)
ENSEMBLE_DIR = tactics/null
export
else
ENSEMBLE_DIR = tactics/ensemble
export
#
# Include the generic caml library
#
INCLUDES += $(CAMLLIB)
#
# Generic phony targets
#
.PHONY: all install clean realclean depend tex doc
#
# Phony target for installing libraries
#
INSTALL_INTERFACES = true
MPINSTALL = mp.install
LMINSTALL = $(MPINSTALL)
.PHONY: $(MPINSTALL)
if $(SSL_ENABLED)
if $(equal $(OSTYPE), Win32)
OCAML_LINK_FLAGS += -cclib $(SSL_LIB_WIN32)/ssleay32MT.lib -cclib $(SSL_LIB_WIN32)/libeay32MT.lib
CFLAGS += /DSSL_ENABLED
INCLUDES += $(SSL_INC_WIN32)
export
else
OCAML_LINK_FLAGS += -cclib -lcrypto -cclib -lssl
CFLAGS += -DSSL_ENABLED
INCLUDES += /usr/kerberos/include
export
export
if $(READLINE_ENABLED)
CFLAGS += $(READLINE_CFLAGS)
OCAML_LINK_FLAGS += -cclib -lreadline
export
if $(NCURSES_ENABLED)
CFLAGS += -DNCURSES
OCAML_LINK_FLAGS += -cclib -lncurses
export
if $(not $(defined MP_DEBUG))
MP_DEBUG[] = $(split :, $(getenv MP_DEBUG, $(EMPTY)))
export
if $(SPELLING_ENABLED)
if $(not $(mem spell, $(MP_DEBUG)))
MP_DEBUG[] += spell
export
export
else
if $(mem spell, $(MP_DEBUG))
MP_DEBUG[] = $(filter-out spell, $(MP_DEBUG))
export
export
setenv(MP_DEBUG, $(concat :, $(MP_DEBUG)))
########################################################################
# .PHONY targets that depend on all the subdirectories.
#
#
# Dependencies are collected in these files
#
THEORIES_PATH = $(file $(EDITOR)/theories.dir)
MLDEBUG_PATH = $(file $(EDITOR)/mldebug.dir)
$(THEORIES_PATH):
section
deps = $(dependencies $@)
deps = $(mapprefix -I, $(in $(EDITOR), $(deps)))
if $(equal $(OSTYPE), Win32)
fprintln($@, $(string $(deps)))
else
fprintln($@, $'INCLUDES='$(quote $(deps)))
$(MLDEBUG_PATH):
section
deps = $(project-directories) $(CAMLLIB) $(CAMLP5LIB)
deps = $(mapprefix -I, $(in $(EDITOR), $(deps)))
if $(equal $(OSTYPE), Win32)
fprintln($@, $(string $(deps)))
else
fprintln($@, $'DEBUGINCLUDES='$(quote $(deps)))
########################################################################
# Default clean command line
#
MLZFILES =
MLPFILES =
CLEAN = $`(RM) *.opt *.run *.o *.obj *.lib *.cm* *.a *~ .*~ .\#* *.ppo *.ppi *.p4i *.p4o .version.* *.omc $`(addsuffix .ml, $(MLZFILES)) $`(addsuffix .mli, $(MLZFILES)) $`(addsuffix .ml, $(MLPFILES))
clean:
$(CLEAN) mk/*.omc $(THEORIES_PATH) $(MLDEBUG_PATH)
rm -rf $(LIB) $(BIN) $(EXPORT)
if $(not $(defined FORCE_REALCLEAN))
FORCE_REALCLEAN = false
export
open build/svn_realclean
realclean: clean
$`(RM) $(find -name *.prlb)
svn_realclean $(if $(FORCE_REALCLEAN), -f) -i .omakedb -i .omakedb.lock -i mk/config -i mk/config.local