diff options
Diffstat (limited to 'src/extraction/Makefile')
| -rw-r--r-- | src/extraction/Makefile | 47 |
1 files changed, 29 insertions, 18 deletions
diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 354dd53..399c5cf 100644 --- a/src/extraction/Makefile +++ b/src/extraction/Makefile @@ -1,45 +1,56 @@ # List of user's files and name of the final program (edit this part) -USERFILES=smtcoq.ml smtcoq.mli -PROGRAM=smtcoq +USERFILES=smtcoq.ml # USERFILES=test.ml -# PROGRAM=test -# USERFILES=../../../../examples/example.ml -# PROGRAM=../../../../examples/example +PROGRAM=smtcoq # Compilation -COQTOP=$(COQBIN)../ +LIB=smtcoq_extr.cmx + +COQLIBPATH=$(shell coqtop -where)/ FLAGS=-rectypes -COMPILEFLAGS=-cclib -lunix +COMPILEFLAGS=-for-pack Smtcoq_extr +PROGRAMFLAGS=-cclib -lunix -linkall +LIBFLAGS=-cclib -lunix -pack -SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../../3rdparty/alt-ergo -COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5 +SMTLIB=-I .. +COQLIB=-I ${COQLIBPATH}kernel -I ${COQLIBPATH}lib -I ${COQLIBPATH}library -I ${COQLIBPATH}parsing -I ${COQLIBPATH}pretyping -I ${COQLIBPATH}interp -I ${COQLIBPATH}proofs -I ${COQLIBPATH}tactics -I ${COQLIBPATH}toplevel -I ${COQLIBPATH}plugins/btauto -I ${COQLIBPATH}plugins/cc -I ${COQLIBPATH}plugins/decl_mode -I ${COQLIBPATH}plugins/extraction -I ${COQLIBPATH}plugins/field -I ${COQLIBPATH}plugins/firstorder -I ${COQLIBPATH}plugins/fourier -I ${COQLIBPATH}plugins/funind -I ${COQLIBPATH}plugins/micromega -I ${COQLIBPATH}plugins/nsatz -I ${COQLIBPATH}plugins/omega -I ${COQLIBPATH}plugins/quote -I ${COQLIBPATH}plugins/ring -I ${COQLIBPATH}plugins/romega -I ${COQLIBPATH}plugins/rtauto -I ${COQLIBPATH}plugins/setoid_ring -I ${COQLIBPATH}plugins/syntax -I ${COQLIBPATH}plugins/xml -I ${COQLIBPATH}clib -I ${COQLIBPATH}gramlib/.pack -I ${COQLIBPATH}engine -I ${COQLIBPATH}config -I ${COQLIBPATH}printing -I ${COQLIBPATH}vernac -I ${COQLIBPATH}plugins/ltac -I ${COQLIBPATH}stm -I ${COQLIBPATH}kernel/byterun + +COQCMX=unix.cmxa threads.cmxa nums.cmxa str.cmxa zarith.cmxa dynlink.cmxa clib.cmxa config.cmxa lib.cmxa gramlib.cmxa kernel.cmxa library.cmxa engine.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa printing.cmxa tactics.cmxa vernac.cmxa stm.cmxa toplevel.cmxa ltac_plugin.cmx micromega_plugin.cmx +SMTCOQCMX=smtcoq_plugin.cmx + +MLIFILES=sat_checker.mli zchaff_checker.mli smt_checker.mli verit_checker.mli +MLFILES=sat_checker.ml zchaff_checker.ml smt_checker.ml verit_checker.ml +CMI=$(MLIFILES:%.mli=%.cmi) +CMX=$(MLFILES:%.ml=%.cmx) -CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa -CMI=extrNative.cmi sat_checker.cmi zchaff_checker.cmi smt_checker.cmi verit_checker.cmi -CMX=extrNative.cmx sat_checker.cmx zchaff_checker.cmx smt_checker.cmx verit_checker.cmx -USERML=$(filter %.ml,$(USERFILES)) -USERCMX=$(USERML:%.ml=%.cmx) USERMLI=$(filter %.mli,$(USERFILES)) +USERML=$(filter %.ml,$(USERFILES)) USERCMI=$(USERMLI:%.mli=%.cmi) +USERCMX=$(USERML:%.ml=%.cmx) OCAMLC=ocamlc OCAMLOPT=ocamlopt +OCAMLFIND=ocamlfind +OCAMLFINDLIB=-I +threads -package zarith -all: $(PROGRAM) +all: $(LIB) $(PROGRAM) %.cmi: %.mli $(OCAMLC) -c $(FLAGS) $(SMTLIB) $(COQLIB) $< %.cmx: %.ml - $(OCAMLOPT) -c $(FLAGS) $(SMTLIB) $(COQLIB) $< + $(OCAMLOPT) -c $(FLAGS) $(COMPILEFLAGS) $(SMTLIB) $(COQLIB) $< + +$(LIB): $(CMI) $(CMX) + $(OCAMLFIND) $(OCAMLOPT) $(FLAGS) $(OCAMLFINDLIB) $(SMTLIB) $(COQLIB) -o $@ $(LIBFLAGS) $(CMX) -$(PROGRAM): $(CMI) $(CMX) $(USERCMI) $(USERCMX) - $(OCAMLOPT) $(FLAGS) $(SMTLIB) $(COQLIB) -o $@ $(COMPILEFLAGS) $(CMXA) $(CMX) $(USERCMX) +$(PROGRAM): $(LIB) $(USERCMI) $(USERCMX) + $(OCAMLFIND) $(OCAMLOPT) $(FLAGS) $(OCAMLFINDLIB) $(SMTLIB) $(COQLIB) -o $@ $(PROGRAMFLAGS) $(COQCMX) $(SMTCOQCMX) $(LIB) $(USERCMX) .PHONY: clean mrproper |