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