diff options
Diffstat (limited to 'src/versions/standard/Makefile.conf')
| -rw-r--r-- | src/versions/standard/Makefile.conf | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/src/versions/standard/Makefile.conf b/src/versions/standard/Makefile.conf new file mode 100644 index 0000000..928db7d --- /dev/null +++ b/src/versions/standard/Makefile.conf @@ -0,0 +1,103 @@ +# This configuration file was generated by running: +# coq_makefile -f Make -o Makefile + + +############################################################################### +# # +# Project files. # +# # +############################################################################### + +COQMF_VFILES = versions/standard/Int63/Int63.v versions/standard/Int63/Int63Native.v versions/standard/Int63/Int63Op.v versions/standard/Int63/Int63Axioms.v versions/standard/Int63/Int63Properties.v versions/standard/Array/PArray.v versions/standard/Structures.v bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v lia/Lia.v spl/Assumptions.v spl/Syntactic.v spl/Arithmetic.v spl/Operators.v Conversion_tactics.v Misc.v SMTCoq.v ReflectFacts.v PropToBool.v BoolToProp.v Tactics.v SMT_terms.v State.v Trace.v +COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.mli trace/satAtom.mli trace/smtAtom.mli trace/smtCertif.mli trace/smtCnf.mli trace/smtCommands.mli trace/smtForm.mli trace/smtMisc.mli trace/smtTrace.mli smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.mli smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli +COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.ml trace/smtMisc.ml trace/smtTrace.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml smtlib2/smtlib2_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml +COQMF_ML4FILES = g_smtcoq.ml4 +COQMF_MLPACKFILES = smtcoq_plugin.mlpack +COQMF_MLLIBFILES = + +############################################################################### +# # +# Path directives (-I, -R, -Q). # +# # +############################################################################### + +COQMF_OCAMLLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' +COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega' +COQMF_COQLIBS = -I . -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/standard -I versions/standard/Int63 -I versions/standard/Array -I '$(shell $(COQBIN)coqc -where)/plugins/micromega' -R . SMTCoq +COQMF_COQLIBS_NOML = -R . SMTCoq + +############################################################################### +# # +# Coq configuration. # +# # +############################################################################### + +COQMF_LOCAL=1 +COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2// +COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/ +COQMF_OCAMLFIND=/usr/bin/ocamlfind +COQMF_CAMLP4=camlp5 +COQMF_CAMLP4O=/usr/bin/camlp5o +COQMF_CAMLP4BIN=/usr/bin/ +COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5 +COQMF_CAMLP4OPTIONS=-loc loc +COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string +COQMF_HASNATDYNLINK=true +COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml +COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2 + +############################################################################### +# # +# Extra variables. # +# # +############################################################################### + +CAMLLEX = $(CAMLBIN)ocamllex +CAMLYACC = $(CAMLBIN)ocamlyacc +COQMF_OTHERFLAGS = +COQMF_INSTALLCOQDOCROOT = SMTCoq + +############################################################################### +# # +# Extra targets. (-extra and -extra-phony, DEPRECATED) # +# # +############################################################################### + +post-all:: + $(MAKE) -f $(SELF) test +clean:: + rm -f test +test : + cd ../unit-tests; make + +post-all:: + $(MAKE) -f $(SELF) ztest +clean:: + rm -f ztest +ztest : + cd ../unit-tests; make zchaff + +post-all:: + $(MAKE) -f $(SELF) vtest +clean:: + rm -f vtest +vtest : + cd ../unit-tests; make verit + +post-all:: + $(MAKE) -f $(SELF) lfsctest +clean:: + rm -f lfsctest +lfsctest : + cd ../unit-tests; make lfsc + +%.ml : %.mll + $(CAMLLEX) $< + +%.ml %.mli : %.mly + $(CAMLYACC) $< + +.PHONY: smtcoq_plugin.mlpack.d +smtcoq_plugin.mlpack.d : verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml + + |