3 include ../Makefile.defs
8 OCAML_FLAGS = -pp $(CAMLP4O)
9 PKGS = -package "$(MATITA_REQUIRES)"
10 CPKGS = -package "$(MATITA_CREQUIRES)"
11 OCAML_THREADS_FLAGS = -thread
12 OCAML_DEBUG_FLAGS = -g
13 OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
14 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
15 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
16 OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
18 MATITA_FLAGS = -noprofile
24 # objects for matita (GTK GUI)
35 matitaGeneratedGui.cmo \
37 applyTransformation.cmo \
41 # objects for matitac (batch compiler)
57 PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
58 PROGRAMS = $(PROGRAMS_BYTE) matitatop
59 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
63 # all: matita.conf.xml $(PROGRAMS) coq.moo
65 # matita.conf.xml: matita.conf.xml.sample
66 # @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
67 # touch matita.conf.xml;\
70 # echo "matita.conf.xml.sample is newer than matita.conf.xml";\
72 # echo "PLEASE update your configuration file!";\
73 # echo "(copying matita.conf.xml.sample should work)";\
78 # coq.moo: library/legacy/coq.ma matitac
79 # ./matitac $(MATITA_FLAGS) $<
80 # coq.moo.opt: library/legacy/coq.ma matitac.opt
81 # ./matitac.opt $(MATITA_FLAGS) $<
83 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
84 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
85 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
86 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
87 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
88 CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES))
89 CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES))
94 ifeq ($(HAVE_OCAMLOPT),yes)
100 matita: matita.ml $(LIB_DEPS) $(CMOS)
102 $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
103 matita.opt: matita.ml $(LIBX_DEPS) $(CMXS)
105 $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
107 dump_moo: dump_moo.ml buildTimeConf.cmo
109 $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $<
110 dump_moo.opt: dump_moo.ml buildTimeConf.cmx
112 $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $<
114 matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
116 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
117 matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
119 $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
121 matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
123 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
126 @test -f $@ || ln -s $< $@
127 matitadep.opt: matitac.opt
128 @test -f $@ || ln -s $< $@
131 @test -f $@ || ln -s $< $@
132 matitaclean.opt: matitac.opt
133 @test -f $@ || ln -s $< $@
136 @test -f $@ || ln -s $< $@
137 matitamake.opt: matitac.opt
138 @test -f $@ || ln -s $< $@
141 @test -f $@ || ln -s $< $@
142 cicbrowser.opt: matita.opt
143 @test -f $@ || ln -s $< $@
145 matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
146 $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
147 $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
151 rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
160 $(MAKE) -C dist/ clean
161 rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
162 rm -f buildTimeConf.ml
163 rm -f matita.glade.bak matita.gladep.bak
164 rm -f matita.conf.xml.sample
171 contribs/LAMBDA-TYPES \
172 contribs/PREDICATIVE-TOPOLOGY \
175 .PHONY: tests tests.opt cleantests cleantests.opt
176 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
177 tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
178 cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
179 cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
181 %-test: matitac matitadep matitaclean coq.moo
182 -cd $* && make -k clean all
183 %-test-opt: matitac.opt matitadep.opt matitaclean.opt coq.moo.opt
184 -cd $* && make -k clean.opt opt
185 %-cleantests: matitaclean
187 %-cleantests-opt: matitaclean.opt
188 -cd $* && make clean.opt
190 # {{{ Distribution stuff
192 ifeq ($(HAVE_OCAMLOPT),yes)
200 ifeq ($(DISTRIBUTED),yes)
202 dist_library: dist_library@library
204 @echo "MATITACLEAN -system all"
205 $(H)./matitaclean$(BEST_EXT) \
206 -system -conffile `pwd`/matita.conf.xml.build all
208 @echo "MATITAMAKE -system init"
209 $(H)MATITA_RT_BASE_DIR=`pwd` \
210 MATITA_FLAGS="-system -conffile `pwd`/matita.conf.xml.build" \
211 ./matitamake$(BEST_EXT) -conffile `pwd`/matita.conf.xml.build \
212 init dist_$* `pwd`/$*
213 @echo "MATITAMAKE -system build"
214 $(H)MATITA_RT_BASE_DIR=`pwd` \
215 MATITA_FLAGS="-system -conffile `pwd`/matita.conf.xml.build" \
216 ./matitamake$(BEST_EXT) -conffile `pwd`/matita.conf.xml.build \
231 gtkmathview.matita.conf.xml \
232 template_makefile.in \
236 ifeq ($(HAVE_OCAMLOPT),yes)
237 INSTALL_STUFF += $(PROGRAMS_OPT)
243 cp -a $(INSTALL_STUFF) $(DEST)
246 STATIC_LINK = dist/static_link/static_link
250 gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
252 gdome gmetadom_gdome_cpp_smart \
257 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
264 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
265 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
267 ifeq ($(HAVE_OCAMLOPT),yes)
268 static: $(STATIC_LINK) $(PROGRAMS_STATIC)
271 @echo "Native code compilation is disabled"
273 @echo "Native code compilation is disabled"
277 $(MAKE) -C dist/ $(STATIC_LINK)
279 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
280 $(STATIC_LINK) $(STATIC_LIBS) -- \
281 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
284 dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
285 $(STATIC_LINK) $(STATIC_CLIBS) -- \
286 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
287 $(STATIC_EXTRA_CLIBS)
289 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
290 $(STATIC_LINK) $(STATIC_CLIBS) -- \
291 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
292 $(STATIC_EXTRA_CLIBS)
294 matitadep.opt.static: matitac.opt.static
295 @test -f $@ || ln -s $< $@
296 matitaclean.opt.static: matitac.opt.static
297 @test -f $@ || ln -s $< $@
298 matitamake.opt.static: matitac.opt.static
299 @test -f $@ || ln -s $< $@
300 cicbrowser.opt.static: matita.opt.static
301 @test -f $@ || ln -s $< $@
302 cicbrowser.opt.static.upx: matita.opt.static.upx
303 @test -f $@ || ln -s $< $@
310 # }}} End of distribution stuff
315 cd ..; otags -vi -r components/ matita/
317 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
321 $(OCAMLDEP) *.ml *.mli > .depend
327 $(H)$(OCAMLC) $(PKGS) -c $<
330 $(H)$(OCAMLC) $(PKGS) -c $<
333 $(H)$(OCAMLOPT) $(PKGS) -c $<
335 @echo "OCAMLC -dtypes $<"
336 $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
339 $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
341 ifeq ($(MAKECMDGOALS),all)
342 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
344 ifeq ($(MAKECMDGOALS),)
345 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
347 ifeq ($(MAKECMDGOALS),opt)
348 $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
351 # vim: set foldmethod=marker: