aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard/Makefile')
-rw-r--r--src/versions/standard/Makefile429
1 files changed, 429 insertions, 0 deletions
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
new file mode 100644
index 0000000..f22a0af
--- /dev/null
+++ b/src/versions/standard/Makefile
@@ -0,0 +1,429 @@
+#############################################################################
+## 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/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
+
generated by cgit (git 2.34.1) at 2024-07-01 11:49:59 +0000