Skip to content

why3
why3
Commit 1620f2f8 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

Coq plugin (in progress)

parent 2942775d
Hide whitespace changes
Inline Side-by-side
Showing with 41 additions and 264 deletions
Makefile.in
View file @ 1620f2f8
......@@ -300,6 +300,26 @@ clean::
rm -f bin/whyide.byte bin/whyide.opt
rm -f src/ide/*.cm[iox] src/ide/*.o src/ide/*.annot
##############
# Coq plugin
##############
byte: coq-plugin-byte-@COQ@
opt: coq-plugin-opt-@COQ@
coq-plugin-byte-yes: src/coq-plugin/whytac.cmo
coq-plugin-byte-no:
coq-plugin-opt-yes: src/coq-plugin/whytac.cmxs
coq-plugin-opt-no:
COQSUBTREES = kernel lib interp parsing proofs pretyping tactics library
src/coq-plugin/whytac.cmo src/coq-plugin/whytac.cmxs: INCLUDES=$(COQSUBTREES:%=-I @COQLIB@/%)
src/coq-plugin/whytac.cmo: BFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: OFLAGS+=-rectypes
src/coq-plugin/whytac.cmxs: $(LIBCMXA) src/coq-plugin/whytac.ml
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
# test targets
##############
......@@ -476,42 +496,28 @@ apidoc: $(APIDOCSRC)
-I +sqlite3 $(APIDOCSRC)
# special rules
###############
# CAMLP4=@CAMLP4O@ pa_extend.cmo pa_macro.cmo
# src/%.cmo: src/%.ml4
# $(OCAMLC) -c $(BFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $<
# src/%.cmx: src/%.ml4
# $(OCAMLOPT) -c $(OFLAGS) -pp "$(CAMLP4) -DOCAML@OCAMLV@ -impl" -impl $<
# src/%.ml: src/%.ml4
# $(CAMLP4) pr_o.cmo -DOCAML@OCAMLV@ -impl $< > $@
# generic rules
###############
.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs .output
.mli.cmi:
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
.ml.cmi:
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
.ml.cmo:
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $<
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
.ml.o:
$(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<
$(OCAMLOPT) -c $(OFLAGS) $<
.ml.cmx:
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $<
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
%.cmxs: %.ml %.cmx
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(INCLUDES) -o $@ $<
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
.mll.ml:
$(OCAMLLEX) $<
......
configure.in
View file @ 1620f2f8
......@@ -202,61 +202,6 @@ else
fi
fi
#looking for ocamlgraph library
LOCALOCAMLGRAPH=no
AC_CHECK_FILE($OCAMLLIB/graph.cmi,OCAMLGRAPH=yes,OCAMLGRAPH=no)
if test "$OCAMLGRAPH" = no ; then
AC_CHECK_FILE($OCAMLLIB/ocamlgraph/graph.cmi,OCAMLGRAPH=yes,OCAMLGRAPH=no)
if test "$OCAMLGRAPH" = no ; then
AC_CHECK_FILE(ocamlgraph/src/sig.mli,OCAMLGRAPH=yes,OCAMLGRAPH=no)
if test "$OCAMLGRAPH" = no ; then
AC_MSG_WARN(Cannot find ocamlgraph library. Please install the *libocamlgraph-ocaml-dev* Debian package - or use the GODI caml package system *http://godi.ocaml-programming.de/* - or compile from sources *http://ocamlgraph.lri.fr/*)
else
OCAMLGRAPHLIB="-I ocamlgraph"
OCAMLGRAPHVER=" in local subdir ocamlgraph"
LOCALOCAMLGRAPH=yes
fi
else
OCAMLGRAPHLIB="-I +ocamlgraph"
OCAMLGRAPHVER=" in Ocaml lib, subdir ocamlgraph"
fi
else
OCAMLGRAPHLIB=""
OCAMLGRAPHVER=" in Ocaml lib, main dir"
fi
# checking ocamlgraph version
dnl AC_MSG_CHECKING(ocamlgraph version)
dnl if $OCAMLC $OCAMLGRAPHLIB graph.cma config/check_ocamlgraph.ml > /dev/null 2>&1 && (test "$OCAMLBEST" = "byte" || $OCAMLOPT $OCAMLGRAPHLIB graph.cmxa config/check_ocamlgraph.ml > /dev/null 2>&1); then
dnl AC_MSG_RESULT(ok)
dnl OCAMLGRAPHVER="0.99"$OCAMLGRAPHVER
dnl else
dnl AC_MSG_RESULT(failed)
dnl if test -d ocamlgraph; then
dnl AC_MSG_RESULT(Switching to local ocamlgraph)
dnl OCAMLGRAPHLIB="-I ocamlgraph"
dnl OCAMLGRAPHVER=" in local subdir ocamlgraph"
dnl LOCALOCAMLGRAPH=yes
dnl else
dnl AC_MSG_ERROR(You need ocamlgraph 0.99b or higher; you may need to compile from sources *http://ocamlgraph.lri.fr/*)
dnl fi
dnl fi
dnl rm -f config/check_ocamlgraph.cmo config/check_ocamlgraph.cmi config/check_ocamlgraph.cmx config/check_ocamlgraph$EXE
dnl # checking local ocamlgraph compilation
dnl if test "$LOCALOCAMLGRAPH" = yes; then
dnl AC_MSG_CHECKING(ocamlgraph compilation)
dnl if (cd ocamlgraph; ./configure && make) > /dev/null 2>&1; then
dnl AC_MSG_RESULT(ok)
dnl else
dnl AC_MSG_ERROR(cannot compile ocamlgraph in ocamlgraph)
dnl fi
dnl fi
# checking for lablgtk2
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,LABLGTK2=yes,LABLGTK2=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,LABLGTK2=yes,LABLGTK2=no)
......@@ -267,54 +212,6 @@ fi
AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# apron library
default_apron=no
APRONLIBS=
AC_ARG_ENABLE(apron,[ --enable-apron=[no/yes] use APRON library for abstract interpretation [default=$default_apron]],,enable_apron=$default_apron)
if test "$enable_apron" = "yes" ; then
AC_CHECK_FILE(/usr/local/lib/apron.cmxa,APRONLIB="-I /usr/local/lib -I /usr/lib",APRONLIB=no)
if test "$APRONLIB" = no ; then
AC_CHECK_FILE(/usr/lib/apron.cmxa,APRONLIB="-I /usr/lib -I /usr/local/lib",APRONLIB=no)
if test "$APRONLIB" = no ; then
AC_MSG_ERROR(Cannot find APRON library.)
fi
fi
APRONLIBS="-cclib ' -lpolka_caml -lpolkaMPQ -loct_caml -loctMPQ -lbox_caml -lboxMPQ -lapron_caml -lapron -lgmp_caml -lmpfr -lgmp -lbigarray -lcamlidl' bigarray.cmxa gmp.cmxa apron.cmxa box.cmxa polka.cmxa"
ATPCMO=atp/atp.cmo
fi
# Frama-C
AC_CHECK_PROG(FRAMAC,frama-c,yes,no)
# camlp4
AC_CHECK_PROG(CAMLP4O,camlp4o,camlp4o,no)
if test "$CAMLP4O" = no ; then
AC_MSG_ERROR(Cannot find camlp4o.)
fi
CAMLP4LIB=`camlp4o -where`
CAMLP4VERSION=`$CAMLP4O -v 2>&1 | sed -n -e 's|.*version *\(.*\)$|\1|p'`
AC_MSG_CHECKING(camlp4 version)
if test "$CAMLP4VERSION" != "$OCAMLVERSION" ; then
AC_MSG_ERROR(differs from ocaml version)
else
AC_MSG_RESULT(ok)
fi
dnl AC_CHECK_PROG(CAMLP4OOPT,camlp4o.opt,camlp4o.opt,no)
dnl if test "CAMLP4OOPT" != no ; then
dnl AC_MSG_CHECKING(camlp4o.opt version)
dnl TMPVERSION=`$CAMLP4OOPT -v 2>&1 |sed -n -e 's|.*version *\(.*\)$|\1|p'`
dnl if test "$TMPVERSION" != $CAMLP4VERSION ; then
dnl AC_MSG_RESULT(differs from camlp4o; camlp4o.opt discarded.)
dnl else
dnl AC_MSG_RESULT(ok)
dnl CAMLP4O=$CAMLP4OOPT
dnl fi
dnl fi
WHYFLOATS=
# Coq
AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then
......@@ -331,109 +228,14 @@ else
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
7.4*)
AC_MSG_RESULT($COQVERSION)
COQC7=$COQC
COQVER=v7
WHYLIBCOQ=lib/coq-v7
cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v;;
8.*|trunk)
AC_MSG_RESULT($COQVERSION)
COQC7="$COQC -v7"
COQC8=$COQC
COQVER=v8
WHYLIBCOQ=lib/coq
cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v
case $COQVERSION in
8.1*|8.2*|trunk)
JESSIELIBCOQ=lib/coq/jessie_why.vo
cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v
COQVER=v8.1
;;
*)
JESSIELIBCOQ=
cp -f lib/coq/WhyCoq8.v lib/coq/WhyCoqCompat.v;;
esac
AC_MSG_CHECKING(Coq floating-point library)
case $COQVERSION in
8.2*|trunk)
if test -f "$COQLIB/user-contrib/AllFloat.vo"; then
AC_MSG_RESULT(yes)
WHYFLOATS="lib/coq/WhyFloats.vo lib/coq/JessieFloats.vo"
COQFLOATSMSG=yes
else
AC_MSG_RESULT(no)
COQFLOATSMSG="no (Coq library AllFloat.vo not found)"
fi
AC_MSG_CHECKING(Coq Gappa library)
if test -f "$COQLIB/user-contrib/Gappa/Gappa_tactic.vo"; then
AC_MSG_RESULT(yes)
WHYFLOATS="$WHYFLOATS lib/coq/JessieGappa.vo"
COQGAPPAMSG=yes
else
AC_MSG_RESULT(no)
COQGAPPAMSG="no (Coq library Gappa_tactic.vo not found)"
fi
;;
*)
COQFLOATSMSG="no (requires Coq version >= 8.2)"
COQGAPPAMSG="no (requires Coq version >= 8.2)"
;;
esac
;;
AC_MSG_RESULT($COQVERSION);;
*)
COQ=no
AC_MSG_WARN(You need Coq 7.4 or later; Coq discarded);;
AC_MSG_WARN(You need Coq 8.x or later; Coq discarded);;
esac
fi
# Alt-ergo
dnl AC_CHECK_PROG(ALTERGO,alt-ergo,alt-ergo,no)
dnl if test "$ALTERGO" = no ; then
dnl AC_CHECK_PROG(ERGO,ergo,ergo,no)
dnl if test "$ERGO" = no ; then
dnl ERGOBIN=alt-ergo
dnl else
dnl ERGOBIN=ergo
dnl fi
dnl else
dnl ERGOBIN=alt-ergo
dnl fi
# PVS
AC_PATH_PROG(PVSC,pvs,no)
if test "$PVSC" = no ; then
PVS=no
AC_MSG_WARN(Cannot find PVS.)
else
PVS=yes
PVSLIB=`pvs -where`/lib
if test "$PVSLIB" = /lib; then
AC_MSG_WARN(PVS found but pvs -where did not work)
PVS=no;
fi
fi
# Mizar
AC_CHECK_PROG(MIZF,mizf,mizf,no)
if test "$MIZF" = no; then
MIZAR=no
AC_MSG_WARN(Cannot find Mizar.)
else
MIZAR=yes
AC_MSG_CHECKING(Mizar library)
if test -d "$MIZFILES"; then
MIZARLIB=$MIZFILES
AC_MSG_RESULT($MIZARLIB)
else if test -d /usr/local/lib/mizar; then
MIZARLIB=$MIZFILES
AC_MSG_RESULT($MIZARLIB)
else
AC_MSG_WARN(Cannot find Mizar library; please set \$MIZFILES)
MIZAR=no
fi
fi
fi
#Viewer for ps and pdf
AC_CHECK_PROGS(PSVIEWER,gv evince)
......@@ -460,39 +262,16 @@ AC_SUBST(LABLGTK2)
AC_SUBST(INCLUDEGTK2)
AC_SUBST(OCAMLWEB)
AC_SUBST(DYNLINK)
# AC_SUBST(CAMLP4O)
# AC_SUBST(CAMLP4LIB)
AC_SUBST(enable_apron)
AC_SUBST(APRONLIB)
AC_SUBST(APRONLIBS)
AC_SUBST(FRAMAC)
AC_SUBST(ATPCMO)
AC_SUBST(FORPACK)
AC_SUBST(COQ)
AC_SUBST(COQC7)
AC_SUBST(COQC8)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVER)
AC_SUBST(WHYLIBCOQ)
AC_SUBST(WHYFLOATS)
AC_SUBST(JESSIELIBCOQ)
# AC_SUBST(ERGOBIN)
AC_SUBST(PVS)
AC_SUBST(PVSC)
AC_SUBST(PVSLIB)
AC_SUBST(MIZAR)
AC_SUBST(MIZF)
AC_SUBST(MIZARLIB)
AC_SUBST(FORPACK)
AC_SUBST(PSVIEWER)
AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile bench/bench src/driver/dynlink_compat.ml)
......@@ -508,29 +287,11 @@ echo " Summary"
echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "OcamlGraph lib : $OCAMLGRAPHVER"
echo "Verbose make : $VERBOSEMAKE"
echo "Why plugin enabled : $enable_dynlink"
echo "Abstract interpretation : $enable_apron"
echo "Frama-C plugin : $FRAMAC"
if test "$enable_apron" = "yes" ; then
echo " APRON lib : $APRONLIB"
fi
echo "GWhy : $LABLGTK2"
echo "Why IDE : $LABLGTK2"
echo "Coq support : $COQ"
if test "$COQ" = "yes" ; then
echo " Version : $COQVER ($COQVERSION)"
if test "$JESSIELIBCOQ" = ""; then
echo " : (Jessie Coq proofs disabled, requires >= 8.1)"
fi
echo " Lib : $COQLIB"
echo " Floats : $COQFLOATSMSG"
echo " Gappa : $COQGAPPAMSG"
fi
# echo "Alt-ergo binary : $ERGOBIN"
echo "PVS support : $PVS"
if test "$PVS" = "yes" ; then
echo " Bin : $PVSC"
echo " Lib : $PVSLIB"
fi
echo "Mizar support : $MIZAR"
src/coq-plugin/whytac.ml 0 → 100644
View file @ 1620f2f8
let x = Why.Ident.id_fresh "x"
let whytac gl =
Tactics.admit_as_an_axiom gl
let _ =
Tacinterp.overwriting_add_tactic "Why" (fun _ -> whytac);
Egrammar.extend_tactic_grammar "Why" [[Egrammar.TacTerm "why"]]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment