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
193 STATIC_LINK = dist/static_link/static_link
197 gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
199 gdome gmetadom_gdome_cpp_smart \
204 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
211 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
212 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
214 ifeq ($(HAVE_OCAMLOPT),yes)
215 static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt
218 @echo "Native code compilation is disabled"
220 @echo "Native code compilation is disabled"
224 $(MAKE) -C dist/ $(STATIC_LINK)
226 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
227 $(STATIC_LINK) $(STATIC_LIBS) -- \
228 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
231 dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
232 $(STATIC_LINK) $(STATIC_CLIBS) -- \
233 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
234 $(STATIC_EXTRA_CLIBS)
236 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
237 $(STATIC_LINK) $(STATIC_CLIBS) -- \
238 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
239 $(STATIC_EXTRA_CLIBS)
241 matitadep.opt.static: matitac.opt.static
242 @test -f $@ || ln -s $< $@
243 matitaclean.opt.static: matitac.opt.static
244 @test -f $@ || ln -s $< $@
245 matitamake.opt.static: matitac.opt.static
246 @test -f $@ || ln -s $< $@
247 cicbrowser.opt.static: matita.opt.static
248 @test -f $@ || ln -s $< $@
249 cicbrowser.opt.static.upx: matita.opt.static.upx
250 @test -f $@ || ln -s $< $@
254 $(MAKE) -C dist/ clean
255 rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
256 rm -f config.log config.status Makefile buildTimeConf.ml
257 rm -f matita.glade.bak matita.gladep.bak
258 rm -rf autom4te.cache/
259 rm -f configure matita.conf.xml.sample
266 # }}} End of distribution stuff
271 cd ..; otags -vi -r ocaml/ matita/
273 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
277 $(OCAMLDEP) *.ml *.mli > .depend
283 $(H)$(OCAMLC) $(PKGS) -c $<
286 $(H)$(OCAMLC) $(PKGS) -c $<
289 $(H)$(OCAMLOPT) $(PKGS) -c $<
291 @echo "OCAMLC -dtypes $<"
292 $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
295 $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
297 ifeq ($(MAKECMDGOALS),all)
298 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
300 ifeq ($(MAKECMDGOALS),)
301 $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
303 ifeq ($(MAKECMDGOALS),opt)
304 $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
307 # vim: set foldmethod=marker: