]> matita.cs.unibo.it Git - helm.git/blob - matita/Makefile
now we try two distinct depend files for compilation in byte and native code
[helm.git] / matita / Makefile
1 export SHELL=/bin/bash
2
3 include ../Makefile.defs
4
5 NULL =
6 H=@
7
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)
17 INSTALL_PROGRAMS= matita matitac
18 INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser 
19 INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover
20
21 MATITA_FLAGS = -noprofile
22 NODB=false
23 ifeq ($(NODB),true)
24         MATITA_FLAGS += -nodb
25 endif
26
27 # objects for matita (GTK GUI)
28 CMOS =                          \
29         buildTimeConf.cmo       \
30         lablGraphviz.cmo        \
31         matitaTypes.cmo         \
32         matitaMisc.cmo          \
33         matitamakeLib.cmo       \
34         matitaInit.cmo          \
35         matitaExcPp.cmo         \
36         matitaEngine.cmo        \
37         matitacLib.cmo          \
38         matitaprover.cmo        \
39         applyTransformation.cmo \
40         matitaGtkMisc.cmo       \
41         matitaScript.cmo        \
42         matitaGeneratedGui.cmo  \
43         matitaMathView.cmo      \
44         matitaGui.cmo           \
45         $(NULL)
46 # objects for matitac (batch compiler)
47 CCMOS =                         \
48         buildTimeConf.cmo       \
49         matitaTypes.cmo         \
50         matitaMisc.cmo          \
51         matitamakeLib.cmo       \
52         matitaInit.cmo          \
53         matitaExcPp.cmo         \
54         matitaEngine.cmo        \
55         matitacLib.cmo          \
56         matitaprover.cmo        \
57         $(NULL)
58 MAINCMOS =                      \
59         matitadep.cmo           \
60         matitaclean.cmo         \
61         matitamake.cmo          \
62         gragrep.cmo             \
63         $(NULL)
64 PROGRAMS_BYTE = \
65         matita matitac cicbrowser matitadep matitaclean matitamake matitaprover
66 PROGRAMS = $(PROGRAMS_BYTE) matitatop
67 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
68 NOINST_PROGRAMS = dump_moo gragrep
69 NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS))
70
71 .PHONY: all
72 all: $(PROGRAMS) $(NOINST_PROGRAMS)
73 #  all: matita.conf.xml $(PROGRAMS) coq.moo
74
75 #  matita.conf.xml: matita.conf.xml.sample
76 #          $(H)if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
77 #                  touch matita.conf.xml;\
78 #          else\
79 #                  echo;\
80 #                  echo "matita.conf.xml.sample is newer than matita.conf.xml";\
81 #                  echo;\
82 #                  echo "PLEASE update your configuration file!";\
83 #                  echo "(copying matita.conf.xml.sample should work)";\
84 #                  echo;\
85 #                  false;\
86 #          fi
87
88 #  coq.moo: library/legacy/coq.ma matitac
89 #          ./matitac $(MATITA_FLAGS) $<
90 #  coq.moo.opt: library/legacy/coq.ma matitac.opt
91 #          ./matitac.opt $(MATITA_FLAGS) $<
92
93 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
94 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
95 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
96 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
97 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
98 CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES))
99 CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES))
100 opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT)
101 upx: $(PROGRAMS_UPX)
102 .PHONY: opt upx
103
104 ifeq ($(HAVE_OCAMLOPT),yes)
105 world: depend.opt opt links
106 else
107 world: depend all
108 endif
109
110 #links %.opt -> %
111 links:
112         $(H)for X in $(INSTALL_PROGRAMS_LINKS_MATITAC) \
113                         $(INSTALL_PROGRAMS_LINKS_MATITA); do\
114                 ln -sf $$X.opt $$X;\
115         done
116         $(H)ln -sf matita.opt matita
117         $(H)ln -sf matitac.opt matitac
118
119 linkonly:
120         $(H)echo "  OCAMLC matita.ml"
121         $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) matita.ml
122         $(H)echo "  OCAMLC matitac.ml"
123         $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) matitac.ml
124 .PHONY: linkonly
125 matita: matita.ml $(LIB_DEPS) $(CMOS)
126         $(H)echo "  OCAMLC $<"
127         $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
128 matita.opt: matita.ml $(LIBX_DEPS) $(CMXS)
129         $(H)echo "  OCAMLOPT $<"
130         $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
131
132 dump_moo: dump_moo.ml buildTimeConf.cmo
133         $(H)echo "  OCAMLC $<"
134         $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $<
135 dump_moo.opt: dump_moo.ml buildTimeConf.cmx
136         $(H)echo "OCAMLOPT $<"
137         $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $<
138
139 matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
140         $(H)echo "  OCAMLC $<"
141         $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
142 matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
143         $(H)echo "  OCAMLOPT $<"
144         $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
145
146 matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
147         $(H)echo "  OCAMLC $<"
148         $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
149
150 matitaprover: matitac
151         $(H)test -f $@ || ln -s $< $@
152 matitaprover.opt: matitac.opt
153         $(H)test -f $@ || ln -s $< $@
154
155 matitadep: matitac
156         $(H)test -f $@ || ln -s $< $@
157 matitadep.opt: matitac.opt
158         $(H)test -f $@ || ln -s $< $@
159
160 matitaclean: matitac
161         $(H)test -f $@ || ln -s $< $@
162 matitaclean.opt: matitac.opt
163         $(H)test -f $@ || ln -s $< $@
164
165 matitamake: matitac
166         $(H)test -f $@ || ln -s $< $@
167 matitamake.opt: matitac.opt
168         $(H)test -f $@ || ln -s $< $@
169         
170 gragrep: matitac
171         $(H)test -f $@ || ln -s $< $@
172 gragrep.opt: matitac.opt
173         $(H)test -f $@ || ln -s $< $@
174         
175 cicbrowser: matita
176         $(H)test -f $@ || ln -s $< $@
177 cicbrowser.opt: matita.opt
178         $(H)test -f $@ || ln -s $< $@
179
180 matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
181         $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
182         $(H)rm -f matitaGeneratedGui.mli
183         $(H)#$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
184
185 .PHONY: clean
186 clean:
187         $(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
188                 $(PROGRAMS) $(PROGRAMS_OPT) \
189                 $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \
190                 $(PROGRAMS_STATIC) \
191                 $(PROGRAMS_UPX) \
192                 $(NULL)
193
194 .PHONY: distclean
195 distclean: clean
196         $(H)$(MAKE) -C dist/ clean
197         $(H)rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
198         $(H)rm -f buildTimeConf.ml
199         $(H)rm -f matita.glade.bak matita.gladep.bak
200         $(H)rm -f matita.conf.xml.sample
201         $(H)rm -rf .matita
202
203 TEST_DIRS =                             \
204         legacy                          \
205         library                         \
206         tests                           \
207         dama                            \
208         contribs/CoRN                   \
209         contribs/RELATIONAL             \
210         contribs/LAMBDA-TYPES           \
211         contribs/PREDICATIVE-TOPOLOGY   \
212         $(NULL)
213
214 .PHONY: tests tests.opt cleantests cleantests.opt
215 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
216 tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
217 cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
218 cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
219
220 %-test: matitac matitadep matitaclean 
221         -cd $* && make -k clean all
222 %-test-opt: matitac.opt matitadep.opt matitaclean.opt
223         -cd $* && make -k clean.opt opt
224 %-cleantests: matitaclean
225         -cd $* && make clean
226 %-cleantests-opt: matitaclean.opt
227         -cd $* && make clean.opt
228
229 # {{{ Distribution stuff
230
231 ifeq ($(DISTRIBUTED),yes)
232
233 dist_library: dist_library@standard-library
234 dist_library@%:
235         $(H)echo "MATITAMAKE init $*"
236         $(H)(cd $(DESTDIR) && ./matitamake init $* $(DESTDIR)/ma/$*)
237         $(H)echo "MATITAMAKE publish $*"
238         $(H)(cd $(DESTDIR) && ./matitamake publish $*)
239         $(H)echo "MATITAMAKE destroy $*"
240         $(H)(cd $(DESTDIR) && ./matitamake destroy $*)
241         touch $@
242
243 endif
244
245 dist_pre: matitaGeneratedGui.ml matitaGeneratedGui.mli
246         $(MAKE) -C dist/ dist_pre
247
248 DESTDIR = $(RT_BASE_DIR)
249 INSTALL_STUFF =                         \
250         icons/                          \
251         help/                           \
252         matita.gtkrc                    \
253         matita.lang                     \
254         matita.ma.templ                 \
255         core_notation.moo               \
256         matita.conf.xml                 \
257         closed.xml                      \
258         gtkmathview.matita.conf.xml     \
259         template_makefile.in            \
260         AUTHORS                         \
261         LICENSE                         \
262         $(NULL)
263
264 ifeq ($(HAVE_OCAMLOPT),yes)
265 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS:%=%.opt) 
266 else
267 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS)
268 endif
269
270 install: install_preliminaries dist_library install_conclusion
271
272 install_preliminaries:
273         install -d $(DESTDIR)/ma/
274         cp -a $(INSTALL_STUFF) $(DESTDIR)
275 ifeq ($(HAVE_OCAMLOPT),yes)
276         install -s $(INSTALL_STUFF_BIN) $(DESTDIR)
277         for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(DESTDIR)/$$p; done
278 else
279         install $(INSTALL_STUFF_BIN) $(DESTDIR)
280 endif
281         for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \
282                 ln -fs matitac $(DESTDIR)/$$p;\
283         done
284         for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \
285                 ln -fs matita $(DESTDIR)/$$p;\
286         done
287         cp -a library/ $(DESTDIR)/ma/standard-library
288         cp -a contribs/ $(DESTDIR)/ma/
289
290 install_conclusion:
291
292 uninstall:
293         rm -rf $(DESTDIR)
294
295 STATIC_LINK = dist/static_link/static_link
296 # for matita
297 STATIC_LIBS =   \
298         t1 t1x  \
299         gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
300         gtksourceview-1.0 \
301         gdome gmetadom_gdome_cpp_smart \
302         stdc++ \
303         mysqlclient \
304         expat \
305         $(NULL)
306 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
307 # for matitac & co
308 STATIC_CLIBS = \
309         gdome \
310         mysqlclient \
311         $(NULL)
312 STATIC_CLIBS_PROVER = \
313         $(STATIC_CLIBS) \
314         z \
315         pcre \
316         expat \
317         xml2 \
318         glib-2.0 \
319         $(NULL)
320 STATIC_EXTRA_CLIBS =
321 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
322 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
323
324 ifeq ($(HAVE_OCAMLOPT),yes)
325 static: $(STATIC_LINK) $(PROGRAMS_STATIC)
326 else
327 upx:
328         $(H)echo "Native code compilation is disabled"
329 static:
330         $(H)echo "Native code compilation is disabled"
331 endif
332
333 $(STATIC_LINK):
334         $(MAKE) -C dist/ $(STATIC_LINK)
335
336 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
337         $(STATIC_LINK) $(STATIC_LIBS) -- \
338                 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
339                 $(STATIC_EXTRA_LIBS)
340         strip $@
341 dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
342         $(STATIC_LINK) $(STATIC_CLIBS) -- \
343                 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
344                 $(STATIC_EXTRA_CLIBS)
345         strip $@
346 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
347         $(STATIC_LINK) $(STATIC_CLIBS) -- \
348                 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
349                 $(STATIC_EXTRA_CLIBS)
350         strip $@
351 matitaprover.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
352         $(STATIC_LINK) $(STATIC_CLIBS_PROVER) -- \
353                 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
354                 $(STATIC_EXTRA_CLIBS);
355         strip $@
356 matitadep.opt.static: matitac.opt.static
357         $(H)test -f $@ || ln -s $< $@
358 matitaclean.opt.static: matitac.opt.static
359         $(H)test -f $@ || ln -s $< $@
360 matitamake.opt.static: matitac.opt.static
361         $(H)test -f $@ || ln -s $< $@
362 cicbrowser.opt.static: matita.opt.static
363         $(H)test -f $@ || ln -s $< $@
364 cicbrowser.opt.static.upx: matita.opt.static.upx
365         $(H)test -f $@ || ln -s $< $@
366
367 %.upx: %
368         cp $< $@
369         strip $@
370         upx $@
371
372 # }}} End of distribution stuff
373
374 tags: TAGS
375 .PHONY: TAGS
376 TAGS:
377         $(H)cd ..; otags -vi -r components/ matita/
378
379 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
380
381 .PHONY: depend
382         
383 depend:
384         $(H)echo "  OCAMLDEP"
385         $(H)$(OCAMLDEP) *.ml *.mli > .depend
386 depend.opt:
387         $(H)echo "  OCAMLDEP -native"
388         $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt
389
390 ifeq ($(MAKECMDGOALS),)
391   include .depend   
392 endif
393
394 ifeq ($(MAKECMDGOALS), all)
395   include .depend   
396 endif
397
398 ifeq ($(MAKECMDGOALS), opt)
399   include .depend.opt   
400 endif
401
402 %.cmi: %.mli
403         $(H)echo "  OCAMLC $<"
404         $(H)$(OCAMLC) $(PKGS) -c $<
405 %.cmo %.cmi: %.ml
406         $(H)echo "  OCAMLC $<"
407         $(H)$(OCAMLC) $(PKGS) -c $<
408 %.cmx: %.ml
409         $(H)echo "  OCAMLOPT $<"
410         $(H)$(OCAMLOPT) $(PKGS) -c $<
411 %.annot: %.ml
412         $(H)echo "  OCAMLC -dtypes $<"
413         $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
414
415 $(CMOS): $(LIB_DEPS)
416 $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
417
418 deps.ps: deps.dot
419         dot -Tps -o $@ $<
420 deps.dot: .depend
421         ./dep2dot.rb < $< | tred > $@
422
423 ifeq ($(MAKECMDGOALS),all)
424    $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
425 endif
426 ifeq ($(MAKECMDGOALS),)
427    $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
428 endif
429 ifeq ($(MAKECMDGOALS),opt)
430    $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
431 endif
432
433 # vim: set foldmethod=marker: