Skip to content

why3
why3
Commit 76504523 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Remove Coq tactic.

parent 95ae6d13
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 16 additions and 1991 deletions
.gitignore
View file @ 76504523
......@@ -159,9 +159,6 @@ why3.conf
# /src/
/src/config.sh
# Coq tactic
/src/coq-tactic/why3tac.ml
# Coq
/lib/coq/version
......
.merlin.in
View file @ 76504523
......@@ -9,7 +9,6 @@ S src/whyml
S src/session
S src/tools
S src/ide
S src/coq-tactic
S src/why3session
S src/why3doc
S src/jessie
......@@ -31,7 +30,6 @@ B src/whyml
B src/session
B src/tools
B src/ide
B src/coq-tactic
B src/why3session
B src/why3doc
B src/jessie
......
CHANGES.md
View file @ 76504523
......@@ -53,7 +53,7 @@ Tools
* deprecated `.why` file extension; use `.mlw` instead
Provers
* deprecated the `why3` Coq tactic
* removed the `why3` Coq tactic :x:
* dropped support for Coq 8.4 :x:
Version 0.88.3, January 11, 2018
......
Makefile.in
View file @ 76504523
......@@ -54,8 +54,6 @@ OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
COQC = @COQC@
COQDEP = @COQDEP@
COQCAMLP = @COQCAMLP@
COQCAMLPLIB = @COQCAMLPLIB@
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
ifeq (@enable_menhirLib@,yes)
......@@ -166,7 +164,6 @@ endif
.PHONY: uninstall-bash uninstall-emacs uninstall-framac
.PHONY: ide install-ide uninstall-ide
.PHONY: coq install-coq uninstall-coq
.PHONY: coq-tactic install-coq-tactic uninstall-coq-tactic
.PHONY: pvs install-pvs uninstall-pvs
.PHONY: install-isabelle
.PHONY: plugins plugins.byte plugins.opt
......@@ -328,10 +325,6 @@ src/mlw/mlinterp.cmx: src/util/debug_optim.cmxs
src/mlw/mlinterp.cmx: OFLAGS += -plugin debug_optim.cmxs
endif
# hide warning 'no cmx file was found in path for module ..., and its interface was not compiled with -opaque' for the coq tactic
src/coq-tactic/why3tac.cmx: WARNINGS:=$(WARNINGS)-58
# build targets
byte: lib/why3/why3.cma
......@@ -965,92 +958,6 @@ install-bin::
install_local:: bin/why3shell
##############
# Coq plugin
##############
ifeq (@enable_coq_tactic@,yes)
COQPGENERATED = src/coq-tactic/why3tac.ml
COQP_FILES = why3tac
COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
$(COQPCMO) $(COQPCMX): BFLAGS += -rectypes
$(COQPCMX): OFLAGS += -rectypes
$(COQPDEP): $(COQPGENERATED)
byte: lib/coq-tactic/why3tac.cma
opt: lib/coq-tactic/why3tac.cmxs
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx, @MENHIRLIB@)
lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@ @WHY3LIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cmo, @MENHIRLIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cma, @ZIPLIB@ @WHY3LIB@)
lib/coq-tactic/why3tac.cmxs: $(WHY3CMXA) $(COQPCMX)
lib/coq-tactic/why3tac.cma: $(WHY3CMA) $(COQPCMO)
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(SHOW) 'Camlp $<'
$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3 -I lib/coq-tactic
ifeq "$(OCAMLBEST)" "opt"
COQTACEXT = cmxs
else
COQTACEXT = cma
COQRTAC += -byte
endif
lib/coq-tactic/Why3.vo: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.$(COQTACEXT)
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) $(COQRTAC) $<
coq-tactic: lib/coq-tactic/Why3.vo
all: coq-tactic
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(COQPDEP)
endif
depend: $(COQPDEP)
CLEANDIRS += src/coq-tactic
CLEANLIBS += lib/coq-tactic/why3tac
GENERATED += $(COQPGENERATED)
clean::
rm -f lib/coq-tactic/*.vo lib/coq-tactic/*.glob
uninstall-coq-tactic:
rm -rf $(LIBDIR)/why3/coq-tactic
install-coq-tactic:
$(MKDIR_P) $(LIBDIR)/why3/coq-tactic
$(INSTALL_DATA) lib/coq-tactic/Why3.vo lib/coq-tactic/why3tac.$(COQTACEXT) $(LIBDIR)/why3/coq-tactic
install:: install-coq-tactic
endif
####################
# Coq realizations
####################
......@@ -1101,11 +1008,7 @@ COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
ifeq (@coq_compat_version@,COQ84)
COQLIBS_BV_FILES = Pow2int
else
COQLIBS_BV_FILES = Pow2int BV_Gen
endif
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
ifeq (@enable_coq_fp_libs@,yes)
......@@ -1836,10 +1739,6 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
@if test "@enable_coq_tactic@" = "yes"; then \
echo ; \
echo "=== Checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic; fi
bench-api:
@echo ""
......@@ -1928,9 +1827,6 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic: lib/coq-tactic/Why3.vo
$(COQC) $(COQRTAC) bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
OCAMLPATH=$(PWD)/lib $(MAKE) -C examples/use_api/runstrat clean
......@@ -2015,7 +1911,7 @@ OCAMLCODE = $(addprefix doc/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
DOC = api glossary ide intro exec macros manpages install \
manual starting syntax syntaxref technical version whyml \
itp pvs coq coq_tactic isabelle
itp pvs coq isabelle
DOCTEX = $(DOC:%=doc/%.tex)
......@@ -2336,7 +2232,7 @@ headers:
Makefile.in configure.in \
src/*/*.ml src/*/*.ml[iyl4] \
plugins/*/*.ml plugins/*/*.ml[ily] \
lib/coq-tactic/*.v lib/coq/*.v lib/coq/*/*.v \
lib/coq/*.v lib/coq/*/*.v \
src/server/*.c src/server/*.h \
src/ide/resetgc.c \
examples/use_api/*.ml
......
ROADMAP
View file @ 76504523
......@@ -222,9 +222,6 @@ and no epsilon
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq tactic
** ajout de bases de hint
* replayer
** deplacer option -bench dans une commande de why3session
......
bench/coq-tactic/test.v deleted 100644 → 0
View file @ 95ae6d13
Require Import Why3.
Inductive Why3Unhabited : Prop := .
Axiom letUsTrustWhy3 : Why3Unhabited.
Ltac ae := why3 "alt-ergo" timelimit 5 ; case letUsTrustWhy3.
Ltac z3 := why3 "z3" timelimit 5; case letUsTrustWhy3.
Require Export ZArith.
Open Scope Z_scope.
Require Export Lists.List.
Section S0.
Variable a:Set->Set.
Goal forall b:Set->Set, forall x:a nat, x=x.
intros; ae.
Qed.
Goal
forall f: (nat->nat)->nat, f S = O -> True.
intros; ae.
Qed.
End S0.
(* Mutually inductive types *)
Inductive tree : Set :=
| Leaf : tree
| Node : Z -> forest -> tree
with forest : Set :=
| Nil : forest
| Cons : tree -> forest -> forest.
Fixpoint tree_size (t:tree) : Z := match t with
| Leaf => 0
| Node _ f => 1 + forest_size f end
with forest_size (f:forest) : Z := match f with
| Nil => 0
| Cons t f => tree_size t + forest_size f end.
Goal tree_size (Node 42 (Cons Leaf Nil)) = 1.
ae.
Qed.
Goal (match Leaf with Leaf => 1 | Node z f => 2 end)=1.
ae.
Qed.
Inductive foo : Set :=
| OO : foo
| SS : forall x:nat, p x -> foo
with p : nat -> Prop :=
| cc : p O.
Goal p O.
(* not a first order goal *)
try ae.
exact cc.
Qed.
Inductive fooo : nat -> Prop :=
c : bar O -> fooo O
with bar : nat -> Prop :=
d : forall f:nat->nat, bar (f O).
Goal fooo O.
(* Don't know *)
try ae.
exact (c (d (fun x => O))).
Qed.
Inductive tree' : Set :=
| Empty' : tree'
| Node' : forest' -> tree'
with forest' : Set :=
| Forest' : (nat -> tree') -> forest'.
Goal forall f: nat ->tree, True.
intros.
ae.
Qed.
Parameter f : (nat -> nat) -> nat.
Goal f (plus O) = f (plus O).
(* not a first order goal *)
try ae.
trivial.
Qed.
Parameter f' : nat -> nat.
Axiom f'_def: f' O = O.
Goal f' (f' O) = O.
ae.
Qed.
Variable b:Set.
Section S.
Variable b:Set->Set.
Variable a:Set.
Inductive sorted : list a -> Prop :=
ccc: sorted (@nil a)
| ddd: forall x: a, sorted (cons x nil).
Variable f : a -> a.
Goal True.
ae.
Qed.
Goal forall x: a, f (f x) = f x -> f (f (f x)) = f x.
intros.
ae.
Qed.
Goal forall l: list a, l=l.
ae.
Qed.
End S.
Goal True.
ae.
Qed.
Parameter par: Z -> Prop.
(* let in *)
Goal
let t := Z in
let f := par 0 in
(forall x:t, par x -> par (let y := x+1 in y)) ->
f -> par 1.
ae.
Qed.
(* cast *)
Goal
(
(forall x:Z, par x -> par (x+1)) -> par (0 : Z) -> par 1 : Prop).
ae.
Qed.
(* type definitions *)
Parameter t : Set -> Set.
Inductive foobar : Set :=
C : t nat -> foobar.
Goal forall x:foobar, x=x.
intros.
ae.
Qed.
(* predicate definition *)
Definition p' (x:nat) := x=O.
Goal p' O.
ae.
Qed.
Goal plus O O = O.
ae.
Qed.
Definition eq' (A:Set) (x y : A) := x=y.
Goal
eq' nat O O.
ae.
Qed.
Definition pred (n:nat) := match n with
| O => O
| S p => p
end.
Goal pred (S O) = O.
ae.
Qed.
(* function definition *)
Definition ff (x:Z) (y:Z) := x+y.
Goal ff 1 2 = 3.
ae.
Qed.
Definition id A (x:A) := x.
Goal id nat O = O.
ae.
Qed.
(* recursive function definition *)
Goal length (cons 1 (cons 2 nil)) = S (S O).
ae.
Qed.
(* recursive predicate definition *)
Goal In 0 (cons 1 (cons 0 nil)).
ae.
Qed.
(* inductive types *)
Parameter P : (nat -> nat) -> Prop.
Goal forall (a:Set), forall x:nat, x=S O -> P S ->
let y := (S (S O)) in S x=y.
intros.
ae.
Qed.
Goal forall (a:Set), forall x:Z, x=1 -> P S -> let y := 2 in x+1=y.
intros.
ae.
Qed.
Goal forall x: list nat, x=x.
intros.
ae.
Qed.
Goal (match (S (S (S O))) with (S (S _)) => True | _ => False end).
ae.
Qed.
Goal
forall a, forall (x: list (list a)),
1<=2 -> match x with nil => 1 | x :: r => 2 end <= 2.
intros a x.
assert (x=nil \/ exists y: list a, exists z:list (list a),
x = cons y z).
destruct x; ae.
ae.
Qed.
(* Polymorphic, Mutually inductive types *)
Inductive ptree {a:Set} : Set :=
| PLeaf : ptree
| PNode : a -> pforest -> ptree
with pforest {a:Set} : Set :=
| PNil : pforest
| PCons : ptree -> pforest -> pforest.
Goal forall x : @ptree Z, x=x.
ae.
Qed.
Definition a := 0+0.
Definition bb := a.
Goal bb=0.
ae.
Qed.
Goal bb=0.
ae.
Qed.
Fixpoint ptree_size {a:Set} (t:@ptree a) : Z := match t with
| PLeaf => 0
| PNode _ f => 1 + pforest_size f end
with pforest_size {a:Set} (f:@pforest a) : Z := match f with
| PNil => 0
| PCons t f => ptree_size t + pforest_size f end.
Goal ptree_size (@PLeaf Z) = 0.
ae.
Qed.
Goal forall (a:Set), ptree_size (@PLeaf a) = 0.
intros.
ae.
Qed.
(* the same, without parameters *)
Inductive ptree' : Type -> Type :=
| PLeaf' : forall (a:Type), ptree' a
| PNode' : forall (a:Type), a -> pforest' a -> ptree' a
with pforest' : Type -> Type :=
| PNil' : forall (a:Type), pforest' a
| PCons' : forall (a:Type), ptree' a -> pforest' a -> pforest' a.
Goal forall x : ptree' Z, x=x.
ae.
Qed.
(* order of type parameters matters *)
Definition wgt (k:(nat * Z)%type) := match k with
| (_, p) => p
end.
Goal wgt (S O, 3) = 3.
ae.
Qed.
Require Import Rbase.
Require Import R_sqrt.
Require Import Rfunctions.
Require Import Rbasic_fun.
Goal forall (x:R), (0 <= x * x)%R.
ae.
Qed.
configure.in
View file @ 76504523
......@@ -92,11 +92,7 @@ AC_ARG_ENABLE(web_ide,
AS_HELP_STRING([--disable-web-ide], [do not build Why3 Web IDE]),,
enable_web_ide=yes)
# Coq tactic and libraries
AC_ARG_ENABLE(coq-tactic,
AS_HELP_STRING([--disable-coq-tactic], [do not build Coq "why3" tactic]),,
enable_coq_tactic=yes)
# Coq libraries
AC_ARG_ENABLE(coq-libs,
AS_HELP_STRING([--disable-coq-libs], [do not build Coq realizations]),,
......@@ -654,15 +650,11 @@ enable_coq_fp_libs=yes
coq_compat_version=
if test "$enable_coq_tactic" = no -a "$enable_coq_libs" = no; then
if test "$enable_coq_libs" = no; then
enable_coq_support=no
reason_coq_support=" (disabled by user)"
fi
if test "$enable_coq_tactic" = no; then
reason_coq_tactic=" (disabled by user)"
fi
if test "$enable_coq_support" = yes; then
AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then
......@@ -678,11 +670,6 @@ if test "$enable_coq_support" = yes; then
COQVERSION=[`$COQC -v | sed -n -e 's|.*version *\([^ ]*\) .*$|\1|p'`]
AC_MSG_RESULT($COQVERSION)
#Even if the name of the variable is CAMLP4 the value can be camlp5
COQCAMLP=[`$COQC -config | sed -n -e 's/CAMLP[45]O=\(.*\)$/\1/p'`]
COQCAMLPLIB=[`$COQC -config | sed -n -e 's/CAMLP[45]LIB=\(.*\)$/\1/p'`]
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
case $COQVERSION in
8.5*)
coq_compat_version="COQ85"
......@@ -695,10 +682,6 @@ if test "$enable_coq_support" = yes; then
;;
8.8*)
coq_compat_version="COQ88"
if test "$enable_coq_tactic" = yes; then
enable_coq_tactic=no
reason_coq_tactic=" (coq <= 8.7 not found)"
fi
;;
*)
enable_coq_support=no
......@@ -718,35 +701,10 @@ if test "$enable_coq_support" = yes; then
fi
if test "$enable_coq_support" = no; then
enable_coq_tactic=no
enable_coq_libs=no
COQVERSION=
fi
if test "$enable_coq_tactic" = yes; then
AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_tactic=no)
if test "$enable_coq_tactic" = no; then
reason_coq_tactic=" ($COQLIB/kernel/term.cmi not found)"
fi
fi
if test "$enable_coq_tactic" = yes; then
if test -z "$COQCAMLP"; then
enable_coq_tactic=no
AC_MSG_WARN(Cannot find camlpXo.)
reason_coq_tactic=" (camlpXo not found)"
fi
fi
if test "$enable_coq_tactic" = yes -a "$OCAMLBEST" = "byte"; then
AC_CHECK_PROG(COQTOPBYTE,coqtop.byte,coqtop.byte,no)
if test "$COQTOPBYTE" = no; then
enable_coq_tactic=no
AC_MSG_WARN(Cannot find coqtop.byte.)
reason_coq_tactic=" (byte compilation needed but coqtop.byte not found)"
fi
fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
......@@ -914,9 +872,6 @@ AC_SUBST(MENHIR)
AC_SUBST(enable_profiling)
AC_SUBST(COQCAMLP)
AC_SUBST(COQCAMLPLIB)
AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)
......@@ -945,16 +900,13 @@ AC_SUBST(enable_menhirLib)
AC_SUBST(MENHIRINCLUDE)
AC_SUBST(MENHIRLIB)
AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_support)
AC_SUBST(enable_coq_fp_libs)
AC_SUBST(coq_compat_version)
AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQPPLIBS)
AC_SUBST(COQVERSION)
AC_SUBST(enable_pvs_libs)
......@@ -1055,7 +1007,6 @@ echo " Coq : $enable_coq_support$reason_coq_support"
if test "$enable_coq_support" = yes ; then
echo " Version : $COQVERSION"
echo " Library path : $COQLIB"
echo " \"why3\" tactic : $enable_coq_tactic$reason_coq_tactic"
echo " Realization support : $enable_coq_libs$reason_coq_libs"
if test "$enable_coq_libs" = yes ; then
echo " FP arithmetic : $enable_coq_fp_libs$reason_coq_fp_libs"
......
doc/coq_tactic.tex deleted 100644 → 0
View file @ 95ae6d13
\subsection{Coq Tactic}
\label{sec:coqtactic}
\why provides a Coq tactic to call external theorem provers as oracles.
This tactic is deprecated and might be removed in future versions of \why.
\subsubsection{Installation}
You need Coq version 8.5 or greater. If this is the case, \why's
configuration detects it, then compiles and installs the Coq tactic.
The Coq tactic is installed in
\begin{center}
\textit{why3-lib-dir}\texttt{/coq-tactic/}
\end{center}
where \textit{why3-lib-dir} is \why's library directory, as reported
by \verb+why3 --print-libdir+. This directory
is automatically added to Coq's load path if you are
calling Coq via \why (from \texttt{why3 ide}, \texttt{why3 replay},
etc.). If you are calling Coq by yourself, you need to add
this directory to Coq's load path using Coq's command line
options \texttt{-I} and \texttt{-R}.
\subsubsection{Usage}
The Coq tactic is called \texttt{why3} and is used as follows:
\begin{center}
\texttt{why3} \verb+"+\textit{prover-name}\verb+"+
$[$\texttt{timelimit} \textit{n}$]$.
\end{center}
The string \textit{prover-name} identifies one of the automated theorem provers
supported by \why, as reported by \verb+why3 --list-provers+
(interactive provers excluded).
\index{list-provers@\verb+--list-provers+}
The tactics translates the current goal to \why's logic and then calls the prover.
If it reports the goal to be valid, then Coq's \texttt{admit}
tactic is used to assume the goal. The prover is called with a time
limit in seconds as given by \why's configuration file
(see Section~\ref{sec:whyconffile}). A different value may be given
using the \texttt{timelimit} keyword.
\subsubsection{Error messages.} The following errors may be reported by
the Coq tactic.
\begin{description}
\item[\texttt{Not a first order goal}]\emptyitem
The Coq goal could not be translated to \why's logic.
\item[\texttt{Timeout}]\emptyitem
There was no answer from the prover within the given time limit.
\item[\texttt{Don't know}]\emptyitem
The prover stopped without validating the goal.
\item[\texttt{Invalid}]\emptyitem
The prover stopped, reporting the goal to be invalid.
\item[\texttt{Failure}]\emptyitem
The prover failed. Depending on the message that follows, you may
want to file a bug report, either to the \why\ developers or to the
prover developers.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% compile-command: "make -C .. doc"
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
doc/install.tex
View file @ 76504523
......@@ -66,12 +66,12 @@ It is also installable from sources, available from the site
\end{itemize}
If you want to use the specific Coq features, \ie the Coq tactic
(Section~\ref{sec:coqtactic}) and Coq realizations
If you want to use the Coq realizations
(Section~\ref{sec:realizations}), then Coq has to be installed before
\why. Look at the summary printed at the end of the configuration
script to check if Coq has been detected properly. Similarly, for
using PVS (Section~\ref{sec:pvs}) or Isabelle (Section~\ref{sec:isabelle}) to discharge proofs, PVS and Isabelle must be
script to check if Coq has been detected properly. Similarly, in order to
use PVS (Section~\ref{sec:pvs}) or Isabelle (Section~\ref{sec:isabelle})
to discharge proofs, PVS and Isabelle must be
installed before \why. You should check that those proof assistants