summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile326
1 files changed, 18 insertions, 308 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 17:22:37 +0000