]> matita.cs.unibo.it Git - helm.git/blob - helm/xmltheory/XmlTheory/Makefile
use a dummy location when no location is provided
[helm.git] / helm / xmltheory / XmlTheory / Makefile
1 ##############################################################################
2 ##                 The Calculus of Inductive Constructions                  ##
3 ##                                                                          ##
4 ##                                Projet Coq                                ##
5 ##                                                                          ##
6 ##                     INRIA                        ENS-CNRS                ##
7 ##              Rocquencourt                        Lyon                    ##
8 ##                                                                          ##
9 ##                                  Coq V7                                  ##
10 ##                                                                          ##
11 ##                                                                          ##
12 ##############################################################################
13
14 # WARNING
15 #
16 # This Makefile has been automagically generated by coq_makefile
17 # Edit at your own risks !
18 #
19 # END OF WARNING
20
21 #
22 # This Makefile was generated by the command line :
23 # coq_makefile -f Make -o Makefile 
24 #
25
26 ##########################
27 #                        #
28 # Variables definitions. #
29 #                        #
30 ##########################
31
32 CAMLP4LIB=`camlp4 -where`
33 MAKE=make "COQBIN=$(COQBIN)" "OPT=$(OPT)"
34 COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
35   -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
36   -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
37   -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
38 ZFLAGS=$(OCAMLLIBS) $(COQSRC)
39 COQFLAGS=-q $(OPT) $(COQLIBS)
40 COQC=$(COQBIN)coqc
41 COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(COQLIBS)
42 GALLINA=gallina
43 COQ2HTML=coq2html
44 COQ2LATEX=coq2latex
45 CAMLC=ocamlc -c
46 CAMLOPTC=ocamlopt -c
47 CAMLLINK=ocamlc
48 CAMLOPTLINK=ocamlopt
49 COQDEP=$(COQBIN)coqdep -c
50 COQVO2XML=coq_vo2xml
51
52 #########################
53 #                       #
54 # Libraries definition. #
55 #                       #
56 #########################
57
58 OCAMLLIBS=-I .\
59   -I $(COQTOP)/contrib/xml
60 COQLIBS=-I .\
61   -R . Bologna.XmlTheory\
62   -I $(COQTOP)/contrib/xml
63
64 ###################################
65 #                                 #
66 # Definition of the "all" target. #
67 #                                 #
68 ###################################
69
70 all: XmlTheory.vo\
71   iXml.cmo\
72   xmltheoryentries.cmo
73
74 spec: XmlTheory.vi
75
76 gallina: XmlTheory.g
77
78 html: XmlTheory.html
79
80 tex: XmlTheory.tex
81
82 gallinatex: XmlTheory.g.tex
83
84 gallinahtml: XmlTheory.g.html
85
86 xml: .xml_time_stamp
87 .xml_time_stamp: XmlTheory.vo
88         $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
89         touch .xml_time_stamp
90
91 ####################
92 #                  #
93 # Special targets. #
94 #                  #
95 ####################
96
97 .PHONY: all opt byte archclean clean install depend xml
98
99 .SUFFIXES: .mli .ml .cmo .cmi .cmx .v .vo .vi .g .html .tex .g.tex .g.html
100
101 .mli.cmi:
102         $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
103
104 .ml.cmo:
105         $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
106
107 .ml.cmx:
108         $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
109
110 .v.vo:
111         $(COQC) $(COQDEBUG) $(COQFLAGS) $*
112
113 .v.vi:
114         $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
115
116 .v.g:
117         $(GALLINA) $<
118
119 .v.html:
120         $(COQ2HTML) $<
121
122 .v.tex:
123         $(COQ2LATEX) $< -latex -o $@
124
125 .v.g.html:
126         $(GALLINA) -stdout $< | $(COQ2HTML) -f > $@
127
128 .v.g.tex:
129         $(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@
130
131 byte:
132         $(MAKE) all "OPT="
133
134 opt:
135         $(MAKE) all "OPT=-opt"
136
137 include .depend
138
139 depend:
140         rm .depend
141         $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
142         $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
143
144 install:
145         @if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
146         cp -f *.vo $(TARGETDIR)
147         cp -f *.cmo $(TARGETDIR)
148
149 Makefile: Make
150         mv -f Makefile Makefile.bak
151         $(COQBIN)coq_makefile -f Make -o Makefile
152
153 clean:
154         rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
155
156 archclean:
157         rm -f *.cmx *.o
158
159 # WARNING
160 #
161 # This Makefile has been automagically generated by coq_makefile
162 # Edit at your own risks !
163 #
164 # END OF WARNING
165