diff options
author | Stephane Glondu <steph@glondu.net> | 2012-09-20 09:41:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-09-20 09:41:14 +0200 |
commit | 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e (patch) | |
tree | ddabcfad1c52bf730690b1be7c900f25dcdf0ec3 /Makefile | |
parent | 9216cffaaa1ef137ef5bdb5b290a930cc6198850 (diff) |
Imported Upstream version 0.3upstream/0.3
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 326 |
1 files changed, 18 insertions, 308 deletions
@@ -1,319 +1,29 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.3 ## -############################################################################# -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING -# -# This Makefile was generated by the command line : -# coq_makefile -R . AAC_tactics -opt MLIFILES = $(MLFILES:.ml=.mli) AAC_coq.ml AAC_helper.ml AAC_search_monad.ml AAC_matcher.ml AAC_theory.ml AAC_print.ml AAC_rewrite.ml AAC.v Instances.v Tutorial.v Caveats.v -f magic.txt -# +FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli rewrite.mli \ + coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \ + aac.mlpack \ + AAC.v Instances.v Tutorial.v Caveats.v -# -# This Makefile may take 3 arguments passed as environment variables: -# - COQBIN to specify the directory where Coq binaries resides; -# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries. -COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g') -CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')" -ifndef CAMLP4BIN - CAMLP4BIN:=$(CAMLBIN) -endif +ARGS := -R . AAC_tactics -CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where) +.PHONY: coq clean -########################## -# # -# Libraries definitions. # -# # -########################## +world: all doc -OCAMLLIBS:= -COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \ - -I $(COQLIB)/library -I $(COQLIB)/parsing \ - -I $(COQLIB)/pretyping -I $(COQLIB)/interp \ - -I $(COQLIB)/proofs -I $(COQLIB)/tactics \ - -I $(COQLIB)/toplevel \ +all: Makefile.coq + $(MAKE) -f Makefile.coq all +coq: Makefile.coq + $(MAKE) -f Makefile.coq +doc: Makefile.coq + $(MAKE) -f Makefile.coq html +Makefile.coq: Makefile $(VS) + coq_makefile $(ARGS) $(FILES) -o Makefile.coq - - - - - - - - - - - - - - - - - -COQLIBS:= -R . AAC_tactics -COQDOCLIBS:=-R . AAC_tactics - -########################## -# # -# Variables definitions. # -# # -########################## - -ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -OPT:= -COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -ifdef CAMLBIN - COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN) -endif -COQC:=$(COQBIN)coqc -COQDEP:=$(COQBIN)coqdep -c -GALLINA:=$(COQBIN)gallina -COQDOC:=$(COQBIN)coqdoc -COQMKTOP:=$(COQBIN)coqmktop -CAMLLIB:=$(shell $(CAMLBIN)ocamlc -where) -CAMLC:=$(CAMLBIN)ocamlc -c -rectypes -CAMLOPTC:=$(CAMLBIN)ocamlopt -c -rectypes -CAMLLINK:=$(CAMLBIN)ocamlc -rectypes -CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes -GRAMMARS:=grammar.cma -CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo -CAMLP4OPTIONS:= -MLIFILES=$(MLFILES:.ml=.mli) -PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl" - -################################### -# # -# Definition of the "all" target. # -# # -################################### - -VFILES:=AAC.v\ - Instances.v\ - Tutorial.v\ - Caveats.v -VOFILES:=$(VFILES:.v=.vo) -GLOBFILES:=$(VFILES:.v=.glob) -VIFILES:=$(VFILES:.v=.vi) -GFILES:=$(VFILES:.v=.g) -HTMLFILES:=$(VFILES:.v=.html) -GHTMLFILES:=$(VFILES:.v=.g.html) -MLFILES:=AAC_coq.ml\ - AAC_helper.ml\ - AAC_search_monad.ml\ - AAC_matcher.ml\ - AAC_theory.ml\ - AAC_print.ml\ - AAC_rewrite.ml -CMOFILES:=$(MLFILES:.ml=.cmo) -CMIFILES:=$(MLFILES:.ml=.cmi) -CMXFILES:=$(MLFILES:.ml=.cmx) -CMXSFILES:=$(MLFILES:.ml=.cmxs) -OFILES:=$(MLFILES:.ml=.o) - -all: $(VOFILES) $(CMOFILES) $(CMXSFILES) doc\ - aac_tactics.cmxs\ - aac_tactics.cmxa\ - aac_tactics.cma\ - .depend -spec: $(VIFILES) - -gallina: $(GFILES) - -html: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES) - -gallinahtml: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES) - -all.ps: $(VFILES) - $(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all-gal.ps: $(VFILES) - $(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all.pdf: $(VFILES) - $(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all-gal.pdf: $(VFILES) - $(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - - - -################### -# # -# Custom targets. # -# # -################### - -doc: $(MLIFILES) - mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc - -aac_tactics.cmxs: $(CMXFILES) - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES) - -aac_tactics.cmxa: $(CMXFILES) - $(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES) - -aac_tactics.cma: $(CMOFILES) - $(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES) - -.depend: $(MLIFILES) - $(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend - -#################### -# # -# Special targets. # -# # -#################### - -.PHONY: all opt byte archclean clean install depend html - -%.cmi: %.mli - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $< - -%.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $< - -%.cmxs: %.ml - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $< - -%.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmxs: %.ml4 - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $< - -%.ml.d: %.ml - $(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) "$<" > "$@" - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -byte: - $(MAKE) all "OPT:=-byte" - -opt: - $(MAKE) all "OPT:=-opt" - -install: - mkdir -p $(COQLIB)/user-contrib - (for i in $(VOFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMOFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMIFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - (for i in $(CMXSFILES); do \ - install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \ - install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \ - done) - -clean: - rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~ - rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) - rm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o) - - rm -rf html - - rm -rf doc - - rm -f aac_tactics.cmxs - - rm -f aac_tactics.cmxa - - rm -f aac_tactics.cma - - rm -f .depend - -archclean: - rm -f *.cmx *.o - - -printenv: - @echo CAMLC = $(CAMLC) - @echo CAMLOPTC = $(CAMLOPTC) - @echo CAMLP4LIB = $(CAMLP4LIB) - -.dummy: magic.txt - mv -f Makefile Makefile.bak - $(COQBIN)coq_makefile -f magic.txt -o Makefile - - --include $(VFILES:.v=.v.d) -.SECONDARY: $(VFILES:.v=.v.d) - --include $(MLFILES:.ml=.ml.d) -.SECONDARY: $(MLFILES:.ml=.ml.d) - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - - - -# override inadequate coq_makefile auto-regeneration -Makefile: make_makefile magic.txt files.txt - ./make_makefile - -# We want to keep the proofs in Caveats and the Tutorial -world: $(VOFILES) doc - - mkdir -p html - $(COQDOC) -toc -utf8 -html -g $(COQDOCLIBS) -d html $(VFILES) - $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Tutorial.v - $(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Caveats.v - -# additional dependencies for AAC (since aac_tactics.cmxs/cma are not -# around the first time we run make, coqdep issues a warning and -# ignores this dependency) -# (one can safely select one of theses dependencies according to -# coq' compilation mode--bytecode or native) -AAC.vo: aac_tactics.cmxa aac_tactics.cmxs aac_tactics.cma - -# .depend contains dependencies for .mli files --include .depend -.SECONDARY: .depend +clean:: Makefile.coq + $(MAKE) -f Makefile.coq clean + rm -f Makefile.coq .depend |