From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 20 Sep 2012 09:41:14 +0200
Subject: Imported Upstream version 0.3

---
 Makefile | 326 ++++-----------------------------------------------------------
 1 file changed, 18 insertions(+), 308 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a56d4b6..1043ce9 100644
--- a/Makefile
+++ b/Makefile
@@ -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
 
-- 
cgit v1.2.3