3 include ../Makefile.defs
14 OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION)
15 OCAMLDEP_FLAGS = -pp $(CAMLP5O)
16 PKGS = -package "$(MATITA_REQUIRES)"
17 CPKGS = -package "$(MATITA_CREQUIRES)"
18 WPKGS = -package "$(MATITA_WREQUIRES)"
19 OCAML_THREADS_FLAGS = -thread
20 OCAML_DEBUG_FLAGS = -g
22 #OCAMLOPT_DEBUG_FLAGS = -p
23 OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
24 OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS)
25 OCAMLTOP = $(OCAMLFIND) ocamlmktop$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS)
26 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) $(SYNTAXOPTIONS)
27 OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS)
28 INSTALL_PROGRAMS= matita matitac
29 INSTALL_PROGRAMS_LINKS_MATITA=
30 INSTALL_PROGRAMS_LINKS_MATITAC= matitaclean
31 MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
34 MATITA_FLAGS = -noprofile
41 matitaScriptLexer.mli \
45 applyTransformation.mli \
52 predefined_virtuals.mli \
59 applyTransformation.mli \
67 applyTransformation.mli \
71 matitaFilesystem.mli \
72 matitaAuthentication.mli \
77 # objects for matita (GTK GUI)
78 ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml)
79 # objects for matitac (batch compiler)
80 CML = buildTimeConf.ml $(CMLI:%.mli=%.ml)
81 WML = buildTimeConf.ml $(WMLI:%.mli=%.ml)
82 MAINCML = $(MAINCMLI:%.mli=%.ml)
85 applyTransformation.ml \
92 matitaGeneratedGui.ml \
94 predefined_virtuals.ml \
102 matitaAuthentication.ml \
108 applyTransformation.mli \
110 matitaFilesystem.mli \
114 predefined_virtuals.mli \
122 matitaScriptLexer.mli \
123 matitaAuthentication.mli \
128 ALL_SYNTAX_ML = matitaScriptLexer.ml
129 ALL_SYNTAX_MLI = matitaScriptLexer.mli
132 matitac matitadaemon matitaclean
133 PROGRAMS = $(PROGRAMS_BYTE)
134 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
136 NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS))
139 all: $(PROGRAMS) $(NOINST_PROGRAMS)
141 UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions)
142 ULEXDIR := $(shell $(OCAMLFIND) query ulex08)
144 matitaScriptLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
145 matitaScriptLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
147 matitaFilesystem.cmi: matitaFilesystem.mli
148 $(H)echo " OCAMLC $<"
149 $(H)$(OCAMLC) $(WPKGS) -c $<
150 matitaFilesystem.cmo: matitaFilesystem.ml
151 $(H)echo " OCAMLC $<"
152 $(H)$(OCAMLC) $(WPKGS) -c $<
154 matitaAuthentication.cmi: matitaAuthentication.mli
155 $(H)echo " OCAMLC $<"
156 $(H)$(OCAMLC) $(WPKGS) -c $<
157 matitaAuthentication.cmo: matitaAuthentication.ml
158 $(H)echo " OCAMLC $<"
159 $(H)$(OCAMLC) $(WPKGS) -c $<
160 matitaAuthentication.cmx: matitaAuthentication.ml
161 $(H)echo " OCAMLOPT $<"
162 $(H)$(OCAMLOPT) $(WPKGS) -c $<
164 CMOS = $(ML:%.ml=%.cmo)
165 CCMOS = $(CML:%.ml=%.cmo)
166 WCMOS = $(WML:%.ml=%.cmo)
167 MAINCMOS = $(MAINCML:%.ml=%.cmo)
168 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
169 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
170 WCMXS = $(patsubst %.cmo,%.cmx,$(WCMOS))
171 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
172 $(CMOS) : $(LIB_DEPS)
173 $(CMXOS): $(LIBX_DEPS)
175 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
176 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
177 CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES))
178 CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES))
179 WLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_WREQUIRES))
180 WLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_WREQUIRES))
181 opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT)
185 ifeq ($(HAVE_OCAMLOPT),yes)
186 world: depend.opt opt links
193 $(H)for X in $(INSTALL_PROGRAMS_LINKS_MATITAC) \
194 $(INSTALL_PROGRAMS_LINKS_MATITA); do\
197 $(H)ln -sf matita.opt matita
198 $(H)ln -sf matitac.opt matitac
201 $(H)echo " OCAMLC matitac.ml"
202 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml
203 $(H)echo " OCAMLC matitadaemon.ml"
204 $(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(WCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml
207 matita: matita.ml $(LIB_DEPS) $(CMOS)
208 $(H)echo " OCAMLC $<"
209 $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
210 matita.opt: matita.ml $(LIBX_DEPS) $(CMXS)
211 $(H)echo " OCAMLOPT $<"
212 $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
214 matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
215 $(H)echo " OCAMLC $<"
216 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
217 matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
218 $(H)echo " OCAMLOPT $<"
219 $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
221 matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(WCMOS) $(MAINCMOS)
222 $(H)echo " OCAMLC $<"
223 $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(WCMOS) $(MAINCMOS) matitadaemon.ml
224 matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(WCMXS) $(MAINCMXS)
225 $(H)echo " OCAMLOPT $<"
226 $(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(WCMXS) $(MAINCMXS) matitadaemon.ml
228 webdb_convert: webdb_convert.ml $(WLIB_DEPS) $(WCMOS) $(MAINCMOS)
229 $(H)echo " OCAMLC $<"
230 $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(WCMOS) $(MAINCMOS) webdb_convert.ml
232 rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
233 $(H)echo " OCAMLC $<"
234 $(H)$(OCAMLC) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMOS) $(MAINCMOS) rottener.ml
235 rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
236 $(H)echo " OCAMLOPT $<"
237 $(H)$(OCAMLOPT) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMXS) $(MAINCMXS) rottener.ml
239 find . -type f -name "*.ma.*.rottened" -exec rm {} \;
242 $(H)test -f $@ || ln -s $< $@
243 matitaclean.opt: matitac.opt
244 $(H)test -f $@ || ln -s $< $@
246 matitaGeneratedGui.ml: matita.glade.utf8
247 $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
249 matita.glade.utf8: matita.glade
250 $(H)xmllint --encode UTF8 $< > $@
254 $(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
255 $(PROGRAMS) $(PROGRAMS_OPT) \
256 rottener rottener.opt \
257 $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \
265 $(H)$(MAKE) -C dist/ clean
266 $(H)rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
267 $(H)rm -f buildTimeConf.ml
268 $(H)rm -f matita.glade.bak matita.gladep.bak
269 $(H)rm -f matita.conf.xml.sample
280 contribs/RELATIONAL \
288 # contribs/LAMBDA-TYPES \
291 .PHONY: tests tests.opt cleantests cleantests.opt
292 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
293 tests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-test-opt)
294 cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
295 cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt)
297 %-test: matitac matitaclean
298 -cd $* && make -k clean all
299 %-test-opt: matitac.opt matitaclean.opt
300 -cd $* && make -k clean.opt opt
301 %-cleantests: matitaclean
303 %-cleantests-opt: matitaclean.opt
304 -cd $* && make clean.opt
306 # {{{ Distribution stuff
308 ifeq ($(DISTRIBUTED),yes)
311 dist_library: install_preliminaries
313 $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes)
315 $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitaclean)
317 $(H)cp $(WHERE)/.matita/matita.db $(WHERE)/metadata.db || true
318 #$(H)rm -rf $(WHERE)/.matita/
323 dist_pre: matitaGeneratedGui.ml
324 $(MAKE) -C dist/ dist_pre
326 WHERE = $(DESTDIR)/$(RT_BASE_DIR)
336 gtkmathview.matita.conf.xml \
341 ifeq ($(HAVE_OCAMLOPT),yes)
342 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS:%=%.opt)
344 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS)
347 install-arch: install_preliminaries
350 install_preliminaries : install_preliminaries.stamp
352 install_preliminaries.stamp:
353 $(H)install -d $(WHERE)/ma/
354 $(H)cp -a $(INSTALL_STUFF) $(WHERE)
355 ifeq ($(HAVE_OCAMLOPT),yes)
356 $(H)install -s $(INSTALL_STUFF_BIN) $(WHERE)
357 $(H)for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(WHERE)/$$p; done
359 $(H)install $(INSTALL_STUFF_BIN) $(WHERE)
361 $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \
362 ln -fs matitac $(WHERE)/$$p;\
364 $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \
365 ln -fs matita $(WHERE)/$$p;\
367 $(H)cp -a library/ $(WHERE)/ma/standard-library
368 $(H)cp -a nlibrary/ $(WHERE)/ma/new-standard-library
370 $(H)touch install_preliminaries.stamp
375 STATIC_LINK = dist/static_link/static_link
379 gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
381 gdome gmetadom_gdome_cpp_smart \
386 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
392 STATIC_CLIBS_PROVER = \
401 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
402 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
404 ifeq ($(HAVE_OCAMLOPT),yes)
405 static: $(STATIC_LINK) $(PROGRAMS_STATIC)
408 $(H)echo "Native code compilation is disabled"
410 $(H)echo "Native code compilation is disabled"
414 $(MAKE) -C dist/ $(STATIC_LINK)
416 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
417 $(STATIC_LINK) $(STATIC_LIBS) -- \
418 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
421 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
422 $(STATIC_LINK) $(STATIC_CLIBS) -- \
423 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
424 $(STATIC_EXTRA_CLIBS)
426 matitaclean.opt.static: matitac.opt.static
427 $(H)test -f $@ || ln -s $< $@
434 # }}} End of distribution stuff
436 # {{{ Deps and automatic rules
440 $(H)cd ..; otags -vi -r components/ matita/
446 $(H)$(OCAMLDEP) $(ALL_NORMAL_ML) $(ALL_NORMAL_MLI) > .depend
447 $(H)$(OCAMLDEP) $(MY_SYNTAXOPTIONS) $(ALL_SYNTAX_ML) $(ALL_SYNTAX_MLI) >> .depend
449 $(H)echo " OCAMLDEP -native"
450 $(H)$(OCAMLDEP) -native $(ALL_NORMAL_ML) $(ALL_NORMAL_MLI) > .depend.opt
451 $(H)$(OCAMLDEP) $(MY_SYNTAXOPTIONS) -native $(ALL_SYNTAX_ML) $(ALL_SYNTAX_MLI) >> .depend.opt
453 # this should be sligtly better, since should work with 'make all opt'
454 MAKECMDGOALS_DELIM=$(addprefix _x_,$(addsuffix _x_,$(MAKECMDGOALS)))
455 ifneq (,$(findstring _x_all_x_,$(MAKECMDGOALS_DELIM)))
456 # if we 'make all opt' the deps for 'all' should be fine also for opt
457 # if we 'make opt all' it should not work...
458 INCLUDE_MANDATORY=yes
460 TO_DEPEND_ON=$(LIB_DEPS)
461 else ifneq (,$(findstring _x_opt_x_,$(MAKECMDGOALS_DELIM)))
462 INCLUDE_MANDATORY=yes
463 TO_INCLUDE+=.depend.opt
464 TO_DEPEND_ON=$(LIBX_DEPS)
465 else ifneq (,$(findstring _x_world_x_,$(MAKECMDGOALS_DELIM)))
466 ifeq ($(HAVE_OCAMLOPT),yes)
467 INCLUDE_MANDATORY=yes
468 TO_INCLUDE+=.depend.opt
469 TO_DEPEND_ON=$(LIBX_DEPS)
471 INCLUDE_MANDATORY=yes
473 TO_DEPEND_ON=$(LIB_DEPS)
478 TO_DEPEND_ON=$(LIB_DEPS)
481 $(MLI:%.mli=%.cmi) $(ML:%.ml=%.cmo) $(ML:%.ml=%.cmx): $(TO_DEPEND_ON)
483 ifeq (no,$(INCLUDE_MANDATORY))
484 -include $(TO_INCLUDE)
486 include $(TO_INCLUDE)
490 $(H)echo " OCAMLC $<"
491 $(H)$(OCAMLC) $(PKGS) -c $<
493 $(H)echo " OCAMLC $<"
494 $(H)$(OCAMLC) $(PKGS) -c $<
496 $(H)echo " OCAMLOPT $<"
497 $(H)$(OCAMLOPT) $(PKGS) -c $<
499 $(H)echo " OCAMLC -dtypes $<"
500 $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
505 ./dep2dot.rb < $< | tred > $@
507 # }}} End of deps and automatic rules
510 # vim: set foldmethod=marker: