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))
62 all: matita.conf.xml $(PROGRAMS) coq.moo
64 matita.conf.xml: matita.conf.xml.sample
65 @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
66 touch matita.conf.xml;\
69 echo "matita.conf.xml.sample is newer than matita.conf.xml";\
71 echo "PLEASE update your configuration file!";\
72 echo "(copying matita.conf.xml.sample should work)";\
77 matita.conf.xml.sample: matita.conf.xml.sample.in
81 @echo "WARNING: The configuration sample file has changed!"
84 coq.moo: library/legacy/coq.ma matitac
85 ./matitac $(MATITA_FLAGS) $<
86 coq.moo.opt: library/legacy/coq.ma matitac.opt
87 ./matitac.opt $(MATITA_FLAGS) $<
89 ifeq ($(HAVE_OCAMLOPT),yes)
91 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
92 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
93 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
94 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
95 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
96 CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES))
97 CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES))
99 opt: $(PROGRAMS_OPT) coq.moo.opt
101 upx: $(PROGRAMS_UPX) coq.moo.opt
106 @echo "Native code compilation is disabled"
110 matita: matita.ml $(LIB_DEPS) $(CMOS)
112 $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
113 matita.opt: matita.ml $(LIBX_DEPS) $(CMXS)
115 $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
117 dump_moo: dump_moo.ml buildTimeConf.cmo
119 $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $<
120 dump_moo.opt: dump_moo.ml buildTimeConf.cmx
122 $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $<
124 matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
126 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
127 matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
129 $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
131 matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
133 $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
136 @test -f $@ || ln -s $< $@
137 matitadep.opt: matitac.opt
138 @test -f $@ || ln -s $< $@
141 @test -f $@ || ln -s $< $@
142 matitaclean.opt: matitac.opt
143 @test -f $@ || ln -s $< $@
146 @test -f $@ || ln -s $< $@
147 matitamake.opt: matitac.opt
148 @test -f $@ || ln -s $< $@
151 @test -f $@ || ln -s $< $@
152 cicbrowser.opt: matita.opt
153 @test -f $@ || ln -s $< $@
155 matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
156 $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
157 $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
161 rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
172 contribs/LAMBDA-TYPES \
173 contribs/PREDICATIVE-TOPOLOGY \
176 .PHONY: tests tests.opt cleantests cleantests.opt
177 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
178 tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
179 cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
180 cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
182 %-test: matitac matitadep matitaclean coq.moo
183 -cd $* && make -k clean all
184 %-test-opt: matitac.opt matitadep.opt matitaclean.opt coq.moo.opt
185 -cd $* && make -k clean.opt opt
186 %-cleantests: matitaclean
188 %-cleantests-opt: matitaclean.opt
189 -cd $* && make clean.opt
191 # {{{ Distribution stuff
194 $(MAKE) MATITA_FLAGS="-system" -C library/
205 gtkmathview.matita.conf.xml \
206 template_makefile.in \
210 ifeq ($(HAVE_OCAMLOPT),yes)
211 INSTALL_STUFF += $(PROGRAMS_OPT)
216 cp -a $(INSTALL_STUFF) $(DEST)
219 STATIC_LINK = dist/static_link/static_link
223 gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
225 gdome gmetadom_gdome_cpp_smart \
230 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
237 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
238 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
240 ifeq ($(HAVE_OCAMLOPT),yes)
241 static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt
244 @echo "Native code compilation is disabled"
246 @echo "Native code compilation is disabled"
250 $(MAKE) -C dist/ $(STATIC_LINK)
252 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
253 $(STATIC_LINK) $(STATIC_LIBS) -- \
254 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
257 dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
258 $(STATIC_LINK) $(STATIC_CLIBS) -- \
259 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
260 $(STATIC_EXTRA_CLIBS)
262 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
263 $(STATIC_LINK) $(STATIC_CLIBS) -- \
264 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
265 $(STATIC_EXTRA_CLIBS)
267 matitadep.opt.static: matitac.opt.static
268 @test -f $@ || ln -s $< $@
269 matitaclean.opt.static: matitac.opt.static
270 @test -f $@ || ln -s $< $@
271 matitamake.opt.static: matitac.opt.static
272 @test -f $@ || ln -s $< $@
273 cicbrowser.opt.static: matita.opt.static
274 @test -f $@ || ln -s $< $@
275 cicbrowser.opt.static.upx: matita.opt.static.upx
276 @test -f $@ || ln -s $< $@
280 $(MAKE) -C dist/ clean
281 rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
282 rm -f config.log config.status Makefile buildTimeConf.ml
283 rm -f matita.glade.bak matita.gladep.bak
284 rm -rf autom4te.cache/
285 rm -f configure matita.conf.xml.sample
292 # }}} End of distribution stuff
297 cd ..; otags -vi -r ocaml/ matita/
299 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
303 $(OCAMLDEP) *.ml *.mli > .depend
309 $(H)$(OCAMLC) $(PKGS) -c $<
312 $(H)$(OCAMLC) $(PKGS) -c $<
315 $(H)$(OCAMLOPT) $(PKGS) -c $<
317 @echo "OCAMLC -dtypes $<"
318 $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
321 $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
323 ifeq ($(MAKECMDGOALS),all)
324 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
326 ifeq ($(MAKECMDGOALS),)
327 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
329 ifeq ($(MAKECMDGOALS),opt)
330 $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
333 # vim: set foldmethod=marker: