diff options
Diffstat (limited to 'src/versions/standard/Makefile')
-rw-r--r-- | src/versions/standard/Makefile | 432 |
1 files changed, 0 insertions, 432 deletions
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile deleted file mode 100644 index 127e8b2..0000000 --- a/src/versions/standard/Makefile +++ /dev/null @@ -1,432 +0,0 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.4pl5 ## -############################################################################# - -# 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 -f Make -o Makefile -# - -.DEFAULT_GOAL := all - -# -# This Makefile may take arguments passed as environment variables: -# COQBIN to specify the directory where Coq binaries resides; -# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; -# DSTROOT to specify a prefix to install path. - -# Here is a hack to make $(eval $(shell works: -define donewline - - -endef -includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) -$(call includecmdwithout@,$(COQBIN)coqtop -config) - -########################## -# # -# Libraries definitions. # -# # -########################## - -OCAMLLIBS?=-I versions/standard\ - -I zchaff\ - -I verit\ - -I trace\ - -I lia\ - -I euf\ - -I cnf -COQLIBS?=-I versions/standard\ - -I zchaff\ - -I verit\ - -I trace\ - -I lia\ - -I euf\ - -I cnf -R . SMTCoq -COQDOCLIBS?=-R . SMTCoq - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLYACC=$(CAMLBIN)ocamlyacc -CAMLLEX=$(CAMLBIN)ocamllex -CMXS=trace/smt_tactic.cmxs -CMXA=trace/smtcoq.cmxa - -OPT?= -COQDEP?="$(COQBIN)coqdep" -c -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -COQCHKFLAGS?=-silent -o -COQDOCFLAGS?=-interpolate -utf8 -COQC?="$(COQBIN)coqc" -GALLINA?="$(COQBIN)gallina" -COQDOC?="$(COQBIN)coqdoc" -COQCHK?="$(COQBIN)coqchk" - -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)tools" -I "$(COQLIB)toplevel" \ - -I "$(COQLIB)plugins/"cc \ - -I "$(COQLIB)plugins/"decl_mode \ - -I "$(COQLIB)plugins/"extraction \ - -I "$(COQLIB)plugins/"field \ - -I "$(COQLIB)plugins/"firstorder \ - -I "$(COQLIB)plugins/"fourier \ - -I "$(COQLIB)plugins/"funind \ - -I "$(COQLIB)plugins/"micromega \ - -I "$(COQLIB)plugins/"nsatz \ - -I "$(COQLIB)plugins/"omega \ - -I "$(COQLIB)plugins/"quote \ - -I "$(COQLIB)plugins/"ring \ - -I "$(COQLIB)plugins/"romega \ - -I "$(COQLIB)plugins/"rtauto \ - -I "$(COQLIB)plugins/"setoid_ring \ - -I "$(COQLIB)plugins/"subtac \ - -I "$(COQLIB)plugins/"subtac/test \ - -I "$(COQLIB)plugins/"syntax \ - -I "$(COQLIB)plugins/"xml -ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) - -CAMLC?=$(OCAMLC) -c -rectypes -CAMLOPTC?=$(OCAMLOPT) -c -rectypes -CAMLLINK?=$(OCAMLC) -rectypes -CAMLOPTLINK?=$(OCAMLOPT) -rectypes -GRAMMARS?=grammar.cma -CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo -CAMLP4OPTIONS?=-loc loc -PP?=-pp '"$(CAMLP4BIN)$(CAMLP4)o" -I "$(CAMLLIB)" -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' - -################## -# # -# Install Paths. # -# # -################## - -ifdef USERINSTALL -XDG_DATA_HOME?="$(HOME)/.local/share" -COQLIBINSTALL=$(XDG_DATA_HOME)/coq -COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq -else -COQLIBINSTALL="${COQLIB}user-contrib" -COQDOCINSTALL="${DOCDIR}user-contrib" -endif - -###################### -# # -# Files dispatching. # -# # -###################### - -VFILES:=Trace.v\ - State.v\ - SMT_terms.v\ - SMTCoq.v\ - Misc.v\ - spl/Operators.v\ - spl/Arithmetic.v\ - spl/Syntactic.v\ - lia/Lia.v\ - euf/Euf.v\ - cnf/Cnf.v\ - versions/standard/Array/PArray.v\ - versions/standard/Int63/Int63Properties.v\ - versions/standard/Int63/Int63Axioms.v\ - versions/standard/Int63/Int63Op.v\ - versions/standard/Int63/Int63Native.v\ - versions/standard/Int63/Ring63.v\ - versions/standard/Int63/Cyclic63.v\ - versions/standard/Int63/Int63Lib.v\ - versions/standard/Int63/Int63.v - --include $(addsuffix .d,$(VFILES)) -.SECONDARY: $(addsuffix .d,$(VFILES)) - -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) -ML4FILES:=trace/smt_tactic.ml4 - --include $(addsuffix .d,$(ML4FILES)) -.SECONDARY: $(addsuffix .d,$(ML4FILES)) - -MLFILES:=lia/lia.ml\ - zchaff/zchaffParser.ml\ - zchaff/zchaff.ml\ - zchaff/satParser.ml\ - zchaff/cnfParser.ml\ - verit/veritSyntax.ml\ - verit/verit.ml\ - verit/veritLexer.ml\ - verit/veritParser.ml\ - verit/smtlib2_util.ml\ - verit/smtlib2_parse.ml\ - verit/smtlib2_lex.ml\ - verit/smtlib2_genConstr.ml\ - verit/smtlib2_ast.ml\ - trace/smtTrace.ml\ - trace/smtMisc.ml\ - trace/smtForm.ml\ - trace/smtCnf.ml\ - trace/smtCertif.ml\ - trace/smtAtom.ml\ - trace/satAtom.ml\ - trace/coqTerms.ml\ - versions/standard/structures.ml - --include $(addsuffix .d,$(MLFILES)) -.SECONDARY: $(addsuffix .d,$(MLFILES)) - -MLIFILES:=verit/veritSyntax.mli\ - trace/smtForm.mli\ - trace/smtAtom.mli - --include $(addsuffix .d,$(MLIFILES)) -.SECONDARY: $(addsuffix .d,$(MLIFILES)) - -ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) -CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES)) -CMXFILES=$(CMOFILES:.cmo=.cmx) -OFILES=$(CMXFILES:.cmx=.o) -CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi)) -CMXSFILES=$(CMXFILES:.cmx=.cmxs) -ifeq '$(HASNATDYNLINK)' 'true' -HASNATDYNLINK_OR_EMPTY := yes -else -HASNATDYNLINK_OR_EMPTY := -endif - -####################################### -# # -# Definition of the toplevel targets. # -# # -####################################### - -all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - mkdir $@ || rm -rf $@/* - $(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) - -spec: $(VIFILES) - -gallina: $(GFILES) - -html: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES) - -gallinahtml: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES) - -all.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -validate: $(VOFILES) - $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=)) - -beautify: $(VFILES:=.beautified) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' - -.PHONY: all opt byte archclean clean install userinstall depend html validate - -################### -# # -# Custom targets. # -# # -################### - -$(CMXS): $(CMXA) - $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ - -$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx - $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ - -ml: verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml - - -%.ml %.mli: %.mly - $(CAMLYACC) $< - -%.ml: %.mll - $(CAMLLEX) $< - -test: - cd ../unit-tests; make - -#################### -# # -# Special targets. # -# # -#################### - -byte: - $(MAKE) all "OPT:=-byte" - -opt: - $(MAKE) all "OPT:=-opt" - -userinstall: - +$(MAKE) USERINSTALL=true install - -install-natdynlink: - for i in $(CMXS); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMXA); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - -install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink) - for i in $(VOFILES); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMXFILES); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - for i in $(CMIFILES); do \ - install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \ - install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - -install-doc: - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html - for i in html/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ - done - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/mlihtml - for i in mlihtml/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ - done - -clean: - rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES) - rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a) - rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES)) - rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) - rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml - - rm -rf $(CMXS) - - rm -rf $(CMXA) - - rm -rf ml - - rm -rf test - - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml - -archclean: - rm -f *.cmx *.o - -printenv: - @"$(COQBIN)coqtop" -config - @echo 'CAMLC = $(CAMLC)' - @echo 'CAMLOPTC = $(CAMLOPTC)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - - -################### -# # -# Implicit rules. # -# # -################### - -%.cmi: %.mli - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.mli.d: %.mli - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -%.ml4.d: %.ml4 - $(COQDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -%.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< - -%.ml.d: %.ml - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.cmxs: %.cmxa - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $< - -%.cmxs: %.cmx - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - |