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