path: root/Makefile

#############################################################################
##  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 
#

# 
# 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

CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)

##########################
#                        #
# Libraries definitions. #
#                        #
##########################

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 \





















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