diff --git a/Makefile.in b/Makefile.in index f6e808dffae6e69d3864e4a1b597d132536f611e..374a54934813f1b9db14799624ff07ec627de10e 100644 --- a/Makefile.in +++ b/Makefile.in @@ -54,6 +54,8 @@ OCAMLDOC = @OCAMLDOC@ OCAMLLIB = @OCAMLLIB@ OCAMLBEST = @OCAMLBEST@ OCAMLVERSION = @OCAMLVERSION@ +COQC = @COQC@ +COQDEP = @COQDEP@ CAMLP5O = @CAMLP5O@ @@ -209,7 +211,6 @@ clean:: install_no_local:: mkdir -p $(BINDIR) - mkdir -p $(LIBDIR)/why3/coq mkdir -p $(DATADIR)/why3/images mkdir -p $(DATADIR)/why3/emacs mkdir -p $(DATADIR)/why3/lang @@ -782,7 +783,7 @@ endif # Coq plugin ############## -ifeq (@enable_coq_support@,yes) +ifeq (@enable_coq_plugin@,yes) COQGENERATED = src/coq-plugin/g_whytac.ml @@ -816,19 +817,58 @@ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4 # depend and clean targets -include .depend.coq +include .depend.coq-plugin -.depend.coq: $(COQGENERATED) +.depend.coq-plugin: $(COQGENERATED) $(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@ -depend: .depend.coq +depend: .depend.coq-plugin clean:: rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs rm -f src/coq-plugin/*.annot src/coq-plugin/*~ rm -f $(COQGENERATED) - rm -f .depend.coq + rm -f .depend.coq-plugin + +endif + +#################### +# Coq realizations +#################### + +ifeq (@enable_coq_libs@,yes) + +COQLIBS_REAL_FILES = Abs MinMax Real Square +COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES)) + +COQLIBS_FILES = $(COQLIBS_REAL) + +COQV = $(addsuffix .v, $(COQLIBS_FILES)) +COQVO = $(addsuffix .vo, $(COQLIBS_FILES)) + +%.vo: %.v + $(COQC) -R lib/coq Why3 $< + +all: $(COQVO) + +install_no_local:: + mkdir -p $(LIBDIR)/why3/coq + mkdir -p $(LIBDIR)/why3/coq/real + cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/ + +install_local: $(COQVO) + +include .depend.coq-libs + +.depend.coq-libs: + $(COQDEP) -slash -R lib/coq Why3 $(COQV) > $@ + +depend: .depend.coq-libs + +clean:: + rm -f $COQVO $(addsuffix .glob, $(COQLIBS_FILES)) + rm -f .depend.coq-libs endif @@ -1126,12 +1166,6 @@ clean:: # .ml4.ml: # $(CAMLP4) pr_o.cmo -impl $< > $@ -# lib/coq/%.vo: lib/coq/%.v -# $(COQC8) -I lib/coq $< - -# lib/coq-v7/%.vo: lib/coq-v7/%.v -# $(COQC7) -I lib/coq-v7 $< - # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile # if test "@enable_apron@" = "yes" ; then \ # echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \ diff --git a/configure.in b/configure.in index c8150255b554c56a6911e4b1d211aa69bc8be5f2..0b887e316a72bb462e38e2701201c0190cddd7a7 100644 --- a/configure.in +++ b/configure.in @@ -77,11 +77,15 @@ AC_ARG_ENABLE(bench, [ --enable-bench enable Why3 benchmarking tool],, enable_bench=yes) -# Coq plugin +# Coq plugin and libraries -AC_ARG_ENABLE(coq-support, - [ --enable-coq-support enable Coq support],, - enable_coq_support=yes) +AC_ARG_ENABLE(coq-plugin, + [ --enable-coq-plugin enable Coq plugin],, + enable_coq_plugin=yes) + +AC_ARG_ENABLE(coq-libs, + [ --enable-coq-libs enable Coq realizations],, + enable_coq_libs=yes) # TPTP parser @@ -363,7 +367,7 @@ dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true) # Coq -if test "$enable_coq_support" = no; then +if test "$enable_coq_plugins" = no -a "$enable_coq_libs" = no; then enable_coq_support=no AC_MSG_WARN(coq support disabled) reason_coq_support=" (disabled by user)" @@ -391,21 +395,36 @@ else esac fi fi -if test "$enable_coq_support" = yes; then - AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no) - if test "$enable_coq_support" = no; then - reason_coq_support=" ($COQLIB/kernel/term.cmi not found)" + +if test "$enable_coq_support" = no; then + enable_coq_plugin=no + enable_coq_libs=no +fi + +if test "$enable_coq_plugin" = yes; then + AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_plugin=no) + if test "$enable_coq_plugin" = no; then + reason_coq_plugin=" ($COQLIB/kernel/term.cmi not found)" fi fi -if test "$CAMLP5O" = no; then - enable_coq_support=no - reason_coq_support=" (camlp5o not found)" +if test "$enable_coq_plugin" = yes -a "$CAMLP5O" = no; then + enable_coq_plugin=no + reason_coq_plugin=" (camlp5o not found)" fi # coq-plugin currently disabled -enable_coq_support=no -reason_coq_support=" (not yet implemented)" +enable_coq_plugin=no +reason_coq_plugin=" (not yet implemented)" + +if test "$enable_coq_libs" = yes; then + AC_CHECK_PROG(COQDEP,coqdep,coqdep,no) + if test "$COQDEP" = no ; then + enable_coq_libs=no + AC_MSG_WARN(Cannot find coqc.) + reason_coq_libs=" (coqdep not found)" + fi +fi # hypothesis_selection @@ -483,7 +502,8 @@ AC_SUBST(SQLITE3LIB) AC_SUBST(enable_bench) AC_SUBST(META_OCAMLGRAPH) -AC_SUBST(enable_coq_support) +AC_SUBST(enable_coq_plugin) +AC_SUBST(enable_coq_libs) AC_SUBST(COQC) AC_SUBST(COQDEP) @@ -528,10 +548,12 @@ echo "Verbose make : $enable_verbose_make" echo "Why IDE : $enable_ide $reason_ide" echo "Why bench tool : $enable_bench" echo "Why documentation : $enable_doc" -echo "Coq plugin support : $enable_coq_support $reason_coq_support" +echo "Coq support : $enable_coq_support $reason_coq_support" if test "$enable_coq_support" = "yes" ; then echo " Version : $COQVERSION" echo " Lib : $COQLIB" + echo " Plugin support : $enable_coq_plugin $reason_coq_plugin" + echo " Realization support : $enable_coq_libs $reason_coq_libs" fi echo "TPTP parser : $enable_whytptp" echo "Menhir library : $enable_menhirlib" diff --git a/lib/coq/.gitignore b/lib/coq/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..480bc6d52d52a260d90534bfb2603a758ce03a87 --- /dev/null +++ b/lib/coq/.gitignore @@ -0,0 +1,2 @@ +*.vo +*.glob