]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/Makefile.common.in
Some more progress in the proof of the (ad-hoc ?) pigeonhole principle.
[helm.git] / helm / ocaml / Makefile.common.in
1 # This Makefile must be included by another one defining:
2 #  $PACKAGE
3 #  $PREDICATES
4 #  $INTERFACE_FILES
5 #  $IMPLEMENTATION_FILES
6 #  $EXTRA_OBJECTS_TO_INSTALL
7 #  $EXTRA_OBJECTS_TO_CLEAN
8 # and put in a directory where there is a .depend file.
9
10 OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
11 OCAMLPATH = @OCAMLFIND_META_DIR@
12
13 PREPROCOPTIONS = -pp camlp4o
14 SYNTAXOPTIONS = -syntax camlp4o
15 PREREQ =
16 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
17 OCAMLDEBUGOPTIONS = -g
18 OCAMLARCHIVEOPTIONS =
19 OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@
20 REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
21 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
22 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS)
23 OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4,$(REQUIRES)" $(SYNTAXOPTIONS)
24 OCAMLLEX = ocamllex
25 OCAMLYACC = ocamlyacc
26
27 OCAMLC_P4 = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
28 OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
29
30 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
31 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
32 LIBRARIES_DEPS = $(foreach X,$(LIBRARIES),$(wildcard \
33         $(shell dirname $(X))/*.mli \
34         $(shell dirname $(X))/*.ml \
35         $(shell dirname $(X))/*/*.ml \
36         $(shell dirname $(X))/*/*.mli))
37
38
39 ARCHIVE = $(PACKAGE).cma
40 ARCHIVE_OPT = $(PACKAGE).cmxa
41 OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \
42                      $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \
43                      $(EXTRA_OBJECTS_TO_INSTALL)
44 DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES)
45
46 $(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES)
47         @if [ $(PACKAGE) != dummy ]; then \
48         echo OCAMLC $@;\
49         $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
50                 $(IMPLEMENTATION_FILES:%.ml=%.cmo); fi
51
52 $(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT)
53         @if [ $(PACKAGE) != dummy ]; then \
54         echo OCAMLOPT $@;\
55         $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
56                 $(IMPLEMENTATION_FILES:%.ml=%.cmx); fi
57
58 prereq: $(PREREQ)
59 all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
60 opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
61 world: all opt
62 test: test.ml $(ARCHIVE)
63         $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
64 test.opt: test.ml $(ARCHIVE_OPT)
65         $(OCAMLOPT) $(ARCHIVE_OPT) -linkpkg -o $@ $<
66
67 depend: $(DEPEND_FILES)
68         $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
69
70 $(PACKAGE).ps: .dep.dot
71         dot -Tps -o $@ $<
72
73 .dep.dot: .depend
74         ocamldot < .depend > $@
75
76 %.cmi: %.mli
77         @echo OCAMLC $<
78         @$(OCAMLC) -c $<
79 %.cmo %.cmi: %.ml
80         @echo OCAMLC $<
81         @$(OCAMLC) -c $<
82 %.cmx: %.ml
83         @echo OCAMLOPT $<
84         @$(OCAMLOPT) -c $<
85 %.annot: %.ml
86         $(OCAMLC) -dtypes $(PKGS) -c $<
87 %.ml %.mli: %.mly
88         $(OCAMLYACC) $<
89 %.ml: %.mll
90         $(OCAMLLEX) $<
91
92 $(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES)
93 $(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS)
94 $(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT)
95
96 clean:
97         rm -f *.cm[ioax] *.cmxa *.o *.a *.annot $(EXTRA_OBJECTS_TO_CLEAN)
98         if [ -f test ]; then rm -f test; else true; fi
99         if [ -f test.opt ]; then rm -f test.opt; else true; fi
100
101 install:
102         mkdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
103         cp $(OBJECTS_TO_INSTALL) $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
104
105 uninstall:
106         cd $(OCAMLFIND_DEST_DIR)/$(PACKAGE) && rm -f $(OBJECTS_TO_INSTALL)
107         rmdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
108
109 backup:
110         cd ..; tar cvzf $(PACKAGE)_$(shell date +%s).tar.gz $(PACKAGE)
111
112 ocamlinit:
113         echo "#use \"topfind\";;" > .ocamlinit
114         echo "#thread;;" >> .ocamlinit
115         for p in $(REQUIRES); do echo "#require \"$$p\";;" >> .ocamlinit; done
116         echo "#load \"$(PACKAGE).cma\";;" >> .ocamlinit
117
118 # $(STATS_EXCLUDE) may be defined in libraries' Makefile to exclude some file
119 # from statistics collection
120 STATS_FILES = \
121         $(shell find . -maxdepth 1 -type f -name \*.ml $(foreach f,$(STATS_EXCLUDE),-not -name $(f))) \
122         $(shell find . -maxdepth 1 -type f -name \*.mli $(foreach f,$(STATS_EXCLUDE),-not -name $(f)))
123 .stats: $(STATS_FILES)
124         rm -f .stats
125         echo -n "LOC:" >> .stats
126         wc -l $(STATS_FILES) | tail -1 | awk '{ print $$1 }' >> .stats
127
128 .PHONY: all opt world backup depend install uninstall clean ocamlinit
129
130 ifneq ($(MAKECMDGOALS), depend)
131    include .depend   
132 endif
133
134 NULL =
135