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