diff options
Diffstat (limited to 'src/Make')
-rw-r--r-- | src/Make | 91 |
1 files changed, 91 insertions, 0 deletions
diff --git a/src/Make b/src/Make new file mode 100644 index 0000000..d1c9342 --- /dev/null +++ b/src/Make @@ -0,0 +1,91 @@ +######################################################################## +## This file is intended to developers, please do not use it to ## +## generate a Makefile, rather use the provided Makefile. ## +######################################################################## + + + + +######################################################################## +## To generate the Makefile: ## +## coq_makefile -f Make -o Makefile ## +## Change the "all" target into: ## +## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## +## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA and VCMXS. ## +## Change the "install" target: change CMO into CMX. ## +## Finally, suppress the "Makefile" target and add to the "clean" target: ## +## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../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 ## +######################################################################## + + +-R . SMTCoq + +-I cnf +-I euf +-I lia +-I trace +-I verit +-I zchaff + +# -custom "cd ../unit-tests; make" "" "logs" +-custom "cd ../unit-tests; make" "" "test" + +-custom "$(CAMLLEX) $<" "%.mll" "%.ml" +-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" +-custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml" + +-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "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" "$(CMXA)" +-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" + +CMXA = trace/smtcoq.cmxa +CMXS = trace/smt_tactic.cmxs +VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi" +CAMLLEX = $(CAMLBIN)ocamllex +CAMLYACC = $(CAMLBIN)ocamlyacc + +trace/coqTerms.ml +trace/satAtom.ml +trace/smtAtom.ml +trace/smtAtom.mli +trace/smtCertif.ml +trace/smtCnf.ml +trace/smtForm.ml +trace/smtForm.mli +trace/smtMisc.ml +trace/smt_tactic.ml4 +trace/smtTrace.ml + +verit/smtlib2_ast.ml +verit/smtlib2_genConstr.ml +verit/smtlib2_lex.ml +verit/smtlib2_parse.ml +verit/smtlib2_util.ml +verit/veritParser.ml +verit/veritLexer.ml +verit/verit.ml +verit/veritSyntax.ml +verit/veritSyntax.mli + +zchaff/cnfParser.ml +zchaff/satParser.ml +zchaff/zchaff.ml +zchaff/zchaffParser.ml + +cnf/Cnf.v + +euf/Euf.v + +lia/lia.ml +lia/Lia.v + +spl/Syntactic.v +spl/Arithmetic.v +spl/Operators.v + +Misc.v +SMTCoq.v +SMT_terms.v +State.v +Trace.v + +# tests/Tests.v |