diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
| commit | a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0 (patch) | |
| tree | 4a934a82dc23b9fa8d0089dc2a95cbbe820733ca /src/extraction/Makefile | |
| parent | 6566176e1f87838bada8c04ba80e608e8c7e958f (diff) | |
| download | smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.tar.gz smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.zip | |
- auto-generated mli files for future documentation
- new Makefiles to handle these mli
Diffstat (limited to 'src/extraction/Makefile')
| -rw-r--r-- | src/extraction/Makefile | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 043afa1..73b0ae4 100644 --- a/src/extraction/Makefile +++ b/src/extraction/Makefile @@ -1,6 +1,6 @@ # List of user's files and name of the final program (edit this part) -USERFILES=smtcoq.ml +USERFILES=smtcoq.ml smtcoq.mli PROGRAM=smtcoq # USERFILES=test.ml # PROGRAM=test @@ -19,9 +19,12 @@ SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../ 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 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 smt_checker.cmi +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 -USERCMX=$(USERFILES:.ml=.cmx) +USERML=$(filter %.ml,$(USERFILES)) +USERCMX=$(USERML:%.ml=%.cmx) +USERMLI=$(filter %.mli,$(USERFILES)) +USERCMI=$(USERMLI:%.mli=%.cmi) OCAMLC=ocamlc OCAMLOPT=ocamlopt @@ -35,7 +38,7 @@ all: $(PROGRAM) %.cmx: %.ml $(OCAMLOPT) -c $(FLAGS) $(SMTLIB) $(COQLIB) $< -$(PROGRAM): $(CMI) $(CMX) $(USERCMX) +$(PROGRAM): $(CMI) $(CMX) $(USERCMI) $(USERCMX) $(OCAMLOPT) $(FLAGS) $(SMTLIB) $(COQLIB) -o $@ $(COMPILEFLAGS) $(CMXA) $(CMX) $(USERCMX) |