]> matita.cs.unibo.it Git - helm.git/blob - matita/Makefile
Debugging code commented out.
[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         library                         \
205         tests                           \
206         dama                            \
207         contribs/CoRN                   \
208         contribs/RELATIONAL             \
209         contribs/LAMBDA-TYPES           \
210         contribs/PREDICATIVE-TOPOLOGY   \
211         $(NULL)
212
213 .PHONY: tests tests.opt cleantests cleantests.opt
214 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
215 tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
216 cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
217 cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
218
219 %-test: matitac matitadep matitaclean 
220         -cd $* && make -k clean all
221 %-test-opt: matitac.opt matitadep.opt matitaclean.opt
222         -cd $* && make -k clean.opt opt
223 %-cleantests: matitaclean
224         -cd $* && make clean
225 %-cleantests-opt: matitaclean.opt
226         -cd $* && make clean.opt
227
228 # {{{ Distribution stuff
229
230 ifeq ($(DISTRIBUTED),yes)
231
232 dist_library: dist_library@standard-library
233 dist_library@%:
234         $(H)echo "MATITAMAKE init $*"
235         $(H)(cd $(DESTDIR) && ./matitamake init $* $(DESTDIR)/ma/$*)
236         $(H)echo "MATITAMAKE publish $*"
237         $(H)(cd $(DESTDIR) && ./matitamake publish $*)
238         $(H)echo "MATITAMAKE destroy $*"
239         $(H)(cd $(DESTDIR) && ./matitamake destroy $*)
240         touch $@
241
242 endif
243
244 dist_pre: matitaGeneratedGui.ml matitaGeneratedGui.mli
245         $(MAKE) -C dist/ dist_pre
246
247 DESTDIR = $(RT_BASE_DIR)
248 INSTALL_STUFF =                         \
249         icons/                          \
250         help/                           \
251         matita.gtkrc                    \
252         matita.lang                     \
253         matita.ma.templ                 \
254         core_notation.moo               \
255         matita.conf.xml                 \
256         closed.xml                      \
257         gtkmathview.matita.conf.xml     \
258         template_makefile.in            \
259         AUTHORS                         \
260         LICENSE                         \
261         $(NULL)
262
263 ifeq ($(HAVE_OCAMLOPT),yes)
264 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS:%=%.opt) 
265 else
266 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS)
267 endif
268
269 install: install_preliminaries dist_library install_conclusion
270
271 install_preliminaries:
272         install -d $(DESTDIR)/ma/
273         cp -a $(INSTALL_STUFF) $(DESTDIR)
274 ifeq ($(HAVE_OCAMLOPT),yes)
275         install -s $(INSTALL_STUFF_BIN) $(DESTDIR)
276         for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(DESTDIR)/$$p; done
277 else
278         install $(INSTALL_STUFF_BIN) $(DESTDIR)
279 endif
280         for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \
281                 ln -fs matitac $(DESTDIR)/$$p;\
282         done
283         for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \
284                 ln -fs matita $(DESTDIR)/$$p;\
285         done
286         cp -a library/ $(DESTDIR)/ma/standard-library
287         cp -a contribs/ $(DESTDIR)/ma/
288
289 install_conclusion:
290
291 uninstall:
292         rm -rf $(DESTDIR)
293
294 STATIC_LINK = dist/static_link/static_link
295 # for matita
296 STATIC_LIBS =   \
297         t1 t1x  \
298         gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
299         gtksourceview-1.0 \
300         gdome gmetadom_gdome_cpp_smart \
301         stdc++ \
302         mysqlclient \
303         expat \
304         $(NULL)
305 STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
306 # for matitac & co
307 STATIC_CLIBS = \
308         gdome \
309         mysqlclient \
310         $(NULL)
311 STATIC_CLIBS_PROVER = \
312         $(STATIC_CLIBS) \
313         z \
314         pcre \
315         expat \
316         xml2 \
317         glib-2.0 \
318         $(NULL)
319 STATIC_EXTRA_CLIBS =
320 PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
321 PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
322
323 ifeq ($(HAVE_OCAMLOPT),yes)
324 static: $(STATIC_LINK) $(PROGRAMS_STATIC)
325 else
326 upx:
327         $(H)echo "Native code compilation is disabled"
328 static:
329         $(H)echo "Native code compilation is disabled"
330 endif
331
332 $(STATIC_LINK):
333         $(MAKE) -C dist/ $(STATIC_LINK)
334
335 matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
336         $(STATIC_LINK) $(STATIC_LIBS) -- \
337                 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
338                 $(STATIC_EXTRA_LIBS)
339         strip $@
340 dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
341         $(STATIC_LINK) $(STATIC_CLIBS) -- \
342                 $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
343                 $(STATIC_EXTRA_CLIBS)
344         strip $@
345 matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
346         $(STATIC_LINK) $(STATIC_CLIBS) -- \
347                 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
348                 $(STATIC_EXTRA_CLIBS)
349         strip $@
350 matitaprover.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
351         $(STATIC_LINK) $(STATIC_CLIBS_PROVER) -- \
352                 $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
353                 $(STATIC_EXTRA_CLIBS);
354         strip $@
355 matitadep.opt.static: matitac.opt.static
356         $(H)test -f $@ || ln -s $< $@
357 matitaclean.opt.static: matitac.opt.static
358         $(H)test -f $@ || ln -s $< $@
359 matitamake.opt.static: matitac.opt.static
360         $(H)test -f $@ || ln -s $< $@
361 cicbrowser.opt.static: matita.opt.static
362         $(H)test -f $@ || ln -s $< $@
363 cicbrowser.opt.static.upx: matita.opt.static.upx
364         $(H)test -f $@ || ln -s $< $@
365
366 %.upx: %
367         cp $< $@
368         strip $@
369         upx $@
370
371 # }}} End of distribution stuff
372
373 tags: TAGS
374 .PHONY: TAGS
375 TAGS:
376         $(H)cd ..; otags -vi -r components/ matita/
377
378 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
379
380 .PHONY: depend
381         
382 depend:
383         $(H)echo "  OCAMLDEP"
384         $(H)$(OCAMLDEP) *.ml *.mli > .depend
385 depend.opt:
386         $(H)echo "  OCAMLDEP -native"
387         $(H)$(OCAMLDEP) -native *.ml *.mli > .depend
388
389 ifneq ($(MAKECMDGOALS), depend)
390  ifneq ($(MAKECMDGOALS), depend.opt)
391    include .depend   
392  endif
393 endif
394
395 %.cmi: %.mli
396         $(H)echo "  OCAMLC $<"
397         $(H)$(OCAMLC) $(PKGS) -c $<
398 %.cmo %.cmi: %.ml
399         $(H)echo "  OCAMLC $<"
400         $(H)$(OCAMLC) $(PKGS) -c $<
401 %.cmx: %.ml
402         $(H)echo "  OCAMLOPT $<"
403         $(H)$(OCAMLOPT) $(PKGS) -c $<
404 %.annot: %.ml
405         $(H)echo "  OCAMLC -dtypes $<"
406         $(H)$(OCAMLC) -dtypes $(PKGS) -c $<
407
408 $(CMOS): $(LIB_DEPS)
409 $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
410
411 deps.ps: deps.dot
412         dot -Tps -o $@ $<
413 deps.dot: .depend
414         ./dep2dot.rb < $< | tred > $@
415
416 ifeq ($(MAKECMDGOALS),all)
417    $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
418 endif
419 ifeq ($(MAKECMDGOALS),)
420    $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
421 endif
422 ifeq ($(MAKECMDGOALS),opt)
423    $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
424 endif
425
426 # vim: set foldmethod=marker: