Commit 012cd7a3 authored by Andrei Paskevich's avatar Andrei Paskevich

Merge branch 'master' into typeinf_api

parents 0ef05cfc 629e530a
......@@ -134,6 +134,12 @@ orphaned-proofs.prf
/lib/pvs/*/*.summary
pvsbin/
# Isabelle
/lib/isabelle/int/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
......@@ -166,6 +172,7 @@ pvsbin/
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
/drivers/isabelle-realizations.aux
# /tests/
/tests/test-jcf/
......
......@@ -8,13 +8,18 @@ The Why3 Verification Platform is developed by
with contributions of
Stefan Berghofer
Sylvie Boldo
Martin Clochard
Simon Cruanes
Leon Gondelman
Daisuke Ishii
Johannes Kanig
David Mentré
Benjamin Monate
Thi-Minh-Tuyen Nguyen
Simão Melo de Sousa
Asma Tafat-Bouzid
Asma Tafat
Piotr Trojanek
Makarius Wenzel
* marks an incompatible change
o shape algorithm modified (see VSTTE'13 paper) but should be
backward compatible
version 0.82, December 12, 2013
===============================
o lemma functions
o polymorphic recursion permitted
o opaque types
o new prover: Metitarski (2.2, contribution by Piotr Trojanek)
o new prover: Metis (2.3)
o new prover: Beagle (0.4.1)
o new prover: Princess (2013-05-13)
o new prover: Yices2 (2.0.4)
o new prover: Isabelle (2013-2, contribution by Stefan Berghofer)
o new version of prover: Alt-Ergo 0.95.2
o new version of prover: CVC4 1.1 & 1.2 & 1.3
o new version of prover: Coq 8.4pl2
o new version of prover: gappa 1.0.0
o new version of prover: SPASS 3.8ds
o new version of prover: veriT (201310)
o API: more examples of use in examples/use_api/
o why3session csv can create graph with option --gnuplot [png|svg|pdf|qt]
o shape algorithm modified (see VSTTE'13 paper) but is
backward compatible thanks to shape_version numbers in
why3session.xml files
* options name and default of why3session csv changed
* [emacs] why.el renamed to why3.el
o [GTK sourceview] why.lang renamed to why3.lang
* [GTK sourceview] why.lang renamed to why3.lang
* Loc.try[1-7] functions now take location as an optional parameter
o [fix] remove extra leading zeros in decimal literals when a prover don't like them
o [fix] PVS output: types are always non-empty
o [fix] PVS: fixed configuration and installation process
o [fix] Coq tactic: now loads dynamic plug-ins
o [fix] bug #15493: correct Coq output for polymorphic algebraic data types
* [fix] wish #15053: Remove proof time from "Goals proved by only one prover" section
of why3session info --stats
o [fix] bug #13736: why3ml was slow when there are many inclusions
o [fix] bug #16488: decimals in TPTP syntax
o [fix] bug #16454: do not send arithmetic triggers anymore to alt-Ergo
o [fix] syntax highlighting bugs: should be fixed by removing the old language
file alt-ergo.lang from alt-ergo distribution
version 0.81, March 25, 2013
============================
......
This diff is collapsed.
......@@ -111,8 +111,96 @@
==================== Roadmap for release 0.83 ========================
== New Features to announce ==
== Final preparation ==
* inform Jerry James <loganjerry@gmail.com> so that he can test the
Fedora package
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* put 0.83 in file Version
* check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600
* check headers
* check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
* do "make dist"
* test distrib/why3-0.83.tar.gz
* install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository
~filliatr/ARCHIVE/www/why)
* put on the web page
- why3-0.83.tar.gz
cp distrib/why3-0.83.tar.gz /users/www-perso/projets/why3/download
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.83.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.83
- why3session.dtd
cp share/why3session.dtd /users/www-perso/projets/why3/
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
make stdlibdoc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.83
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.83 \
/users/www-perso/projets/why3/stdlib
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
make apidoc
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.83
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.83 \
/users/www-perso/projets/why3/api
(PROBLEME avec style.css ? Ou est le probleme ?)
- update the main HTML page (sources are in repository why3-www)
edit index.html
make export
- add links to extra resources like
http://why3.lri.fr/jfla-2012/, http://www.lri.fr/~marche/MPRI-2-36-1/,
page du cours de l'X (in french ? using Krakatoa/why3 bridge)
- make everything writeable for the group
chmod -R g+w /users/www-perso/projets/why3
* make a last commit:
- git commit -m "release 0.83"
- add tag 0.83 to the git repository, using
git tag 0.83
- do not forget to push it using
git push
git push --tags
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* produce the Why3 part of Toccata gallery
-> add also a tar.gz and a ZIP file of it (this is done by doing
"make gallery-files" in the sources of the Toccata web pages)
* Announce the distrib
- What to put in the announcement: see New Features above
* The next commit : add +git to the version in file Version
== TODOs ==
* eliminate_match:
** faire un cas particulier pour "bool", le match pouvant se traduire
vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match
poymorphe.
* extraction vers Caml
** utiliser ZArith
......@@ -139,32 +227,32 @@
* detect editors
*** check if coqide and also emacs/proof-general is installed
* bug 15629
* bug #15629
==================== Roadmap for release 0.82 ========================
Scheduled for 31 october 2013
Scheduled for 9 december 2013
== New Features to announce ==
* input language
** lemma functions
** polymorphic recursion permitted
** types "opaques" ???
** types "opaques" TODO ???
* new provers:
** veriT 201310
** Metitarski 2.2
** Metitarski 2.2 (contribution by Piotr Trojanek)
** Metis 2.3
** Beagle 0.4.1
** Princess 2013-05-13
** Yices2 2.0.4
** Isabelle 2013-2 (contribution by Stefan Berghofer)
* new versions of provers:
** Alt-Ergo 0.95.2
** CVC4 1.1 (& 1.2 ?)
** CVC4 1.1 & 1.2 & 1.3
** Coq 8.4pl2
** gappa 1.0.0
** SPASS 3.8ds
......@@ -175,10 +263,9 @@ Scheduled for 31 october 2013
* why3session
** --stats: changed (detailler, temps, distinction root et subgoals, CLAUDE)
** --hist: TODO documenter (voir Alain ou Mohamed sur les graphes SMT)
* bug fixes:
** remove extra leading zeros in decimal literals when a prover don't like them
** remove extra leading zeros in decimal literals when a prover don't like them
** PVS output: types are always non-empty
** PVS: fixed configuration and installation process
** improved shape mecanism for session updates (see VSTTE'13 paper).
......@@ -186,9 +273,11 @@ Scheduled for 31 october 2013
assured.
** Coq tactic: now loads dynamic plug-ins
** Coq output: fixed printing of polymorphic recursive datatypes
** bug #15493: ?
** bug #15053: ?
** bug #13736: ?
** bug #15493: correct Coq output for polymorphic algebraic data types
** wish #15053: Remove proof time from "Goals proved by only one prover" section of why3session info --stats
** bug #13736: why3ml was slow when there are many inclusions
** bug #16488: decimals in TPTP syntax
** bug #16454: do not send arithmetic triggers anymore to alt-Ergo
** syntax highlighting bugs: should be fixed by removing the old language
file alt-ergo.lang from alt-ergo distribution
......@@ -197,15 +286,15 @@ Scheduled for 31 october 2013
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate" is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* put 0.82 in file Version
* check headers
* check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out
in ./macros.tex, and then "make doc"
* manual in HTML: "make doc/html/index.html"
* do "make distrib"
(check that manual in HTML is also generated, doc/html/index.html)
* do "make dist"
* test distrib/why3-0.82.tar.gz
* install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository
......@@ -235,7 +324,7 @@ Scheduled for 31 october 2013
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.82 \
/users/www-perso/projets/why3/api
PROBLEME avec style.css
(PROBLEME avec style.css ? Ou est le probleme ?)
- update the main HTML page (sources are in repository why3-www)
edit index.html
make export
......@@ -267,19 +356,11 @@ Scheduled for 31 october 2013
== TODOs ==
* Patch de johannes pour les noms de fichier pour Isabelle TODO
* DONE Patch de johannes pour les noms de fichier pour Isabelle
* discriminate, mettre les bons arguments par defaut (ANDREI)
DONE ?
* eliminate_match: (apres la release ?)
** faire un cas particulier pour "bool", le match pouvant se traduire
vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match
poymorphe.
* DONE discriminate, mettre les bons arguments par defaut (ANDREI)
* efficiency issues
* DONE efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** prouveur de Martin
** tester avant la release sur
......@@ -311,18 +392,18 @@ Scheduled for 31 october 2013
transformations, write new functions on terms
- LEON: add a section "further reading"
* bug fix: 16454 (ne pas envoyer des triggers arithmetiques) (GUILLAUME)
* DONE bug fix: 16454 (ne pas envoyer des triggers arithmetiques) (GUILLAUME)
* bug fix: 15652 (ghost code detection)
* DONE bug fix: 15652 (ghost code detection)
* support for new provers
** Alt-Ergo 0.95.2 DONE
** CVC4 1.2 TODO: pb avec les booleens
** CVC4 1.2 DONE: pb avec les booleens
** DONE Coq 8.4pl2: probleme tactique Why3
** DONE ? Metitarski: improve it (CLAUDE, GUILLAUME)
** DONE Metitarski: improve it (CLAUDE, GUILLAUME)
* DONE? simplification de (a && false) ne devrait pas etre false
* DONE simplification de (a && false) ne devrait pas etre false
......
# Why version
VERSION=0.81+git
VERSION=0.82+git
......
......@@ -97,6 +97,12 @@ AC_ARG_ENABLE(pvs-libs,
[ --enable-pvs-libs enable PVS realizations],,
enable_pvs_libs=yes)
# Isabelle libraries
AC_ARG_ENABLE(isabelle-libs,
[ --enable-isabelle-libs enable Isabelle realizations],,
enable_isabelle_libs=yes)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -527,6 +533,41 @@ else
COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
fi
# Isabelle
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
AC_MSG_WARN(Isabelle support disabled)
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
if test "$ISABELLE" = no ; then
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
2013-2)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-2; Isabelle discarded)
reason_isabelle_support=" (need version 2013-2)"
;;
esac
fi
fi
if test "$enable_isabelle_support" = no; then
enable_isabelle_libs=no
fi
if test "$enable_pvs_libs" = yes; then
AC_MSG_CHECKING([for NASA PVS library])
enable_pvs_libs=no
......@@ -654,6 +695,10 @@ AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
AC_SUBST(COMPILETIMEPVS)
AC_SUBST(enable_isabelle_libs)
AC_SUBST(ISABELLE)
AC_SUBST(ISABELLEVERSION)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
......@@ -725,6 +770,11 @@ if test "$enable_pvs_support" = yes ; then
echo " Library path : $PVSLIB"
echo " Realization support : $enable_pvs_libs$reason_pvs_libs"
fi
echo "Isabelle support : $enable_isabelle_support$reason_isabelle_support"
if test "$enable_isabelle_support" = yes ; then
echo " Version : $ISABELLEVERSION"
echo " Realization support : $enable_isabelle_libs$reason_isabelle_libs"
fi
echo "Frama-C support : $enable_frama_c$reason_frama_c"
if test "$enable_frama_c" = yes ; then
echo " Version : $FRAMAC_VERSION"
......
\subsection{Isabelle/HOL}
When using Isabelle, files generated from Why3 theories are stored in
a dedicated XML format. Those files should not be edited. Instead,
realizations must be designed in some \texttt{.thy} as follows. See
directory \url{lib/isabelle} for examples.
The realization file corresponding to some Why3 file \url{f.why}
should have the following form.
\begin{verbatim}
theory Why3_f
imports Why3_Setup
begin
section {* realization of theory T *}
why3_open "f/T.xml"
why3_vc <some lemma>
<proof>
why3_vc <some other lemma> by proof
[...]
why3_end
\end{verbatim}
......@@ -104,7 +104,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, March 2013
Version \whyversion{}, December 2013
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -201,8 +201,11 @@ Report any bug to the \why Bug Tracking System:
\subsection*{Acknowledgements}
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, Leon Gondelman, Johannes Kanig, St\'ephane
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\cleardoublepage
......
......@@ -29,8 +29,10 @@ realization:
\texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}.
\item insert anything between generated declarations, such as a lemma,
an extra definition for the purpose of a proof, etc.
an extra definition for the purpose of a proof, an extra
\texttt{IMPORTING} command, etc. Do not forget to surround these
extra declarations with blank lines.
\end{itemize}
\why makes some effort to merge the new declarations with the old ones
and with the user chunks. If it happens that some chunks could not be
\why makes some effort to merge new declarations with old ones
and with user chunks. If it happens that some chunks could not be
merged, they are appended at the end of the file, in comments.
......@@ -101,6 +101,8 @@ comment.
\input{./pvs.tex}
\input{./isabelle.tex}
\section{Shipping libraries of realizations}
While modifying an existing driver file might be sufficient for local
......
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_projections"
transformation "simplify_formula"
theory BuiltIn
syntax type int "<type name=\"Int.int\"/>"
syntax type real "<type name=\"Real.real\"/>"
syntax predicate (=) "<app><const name=\"HOL.eq\"/>%1%2</app>"
end
theory Bool
syntax type bool "<type name=\"HOL.bool\"/>"
syntax function True "<const name=\"HOL.True\"/>"
syntax function False "<const name=\"HOL.False\"/>"
end
theory bool.Bool
syntax function andb "<app><const name=\"HOL.conj\"/>%1%2</app>"
syntax function orb "<app><const name=\"HOL.disj\"/>%1%2</app>"
syntax function notb "<app><const name=\"HOL.Not\"/>%1</app>"
syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
end
theory int.Int
syntax function zero "<number val=\"0\"><type name=\"Int.int\"/></number>"
syntax function one "<number val=\"1\"><type name=\"Int.int\"/></number>"
syntax function (+) "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
syntax function (-) "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
syntax function (*) "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"
syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
syntax predicate (<) "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
syntax predicate (>) "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
end
theory int.Abs
syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
remove prop Abs_pos
end
theory int.MinMax
syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
end
theory int.Exponentiation
syntax function power "<app><const name=\"Power.power_class.power\"/>%1<app><const name=\"Int.nat\"/>%2</app></app>"
end
theory list.List
syntax type list "<type name=\"List.list\">%1</type>"
syntax function Nil "<const name=\"List.list.Nil\">%t0</const>"
syntax function Cons "<app><const name=\"List.list.Cons\"/>%1%2</app>"
end
theory list.Length
syntax function length "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"List.length\"/>%1</app></app>"
end
theory list.Append
syntax function (++) "<app><const name=\"List.append\"/>%1%2</app>"
end
theory list.Reverse
syntax function reverse "<app><const name=\"List.rev\"/>%1</app>"
end
theory list.Mem
syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.set\"/>%2</app></app>"
end
theory list.NthNoOpt
syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
end
theory option.Option
syntax type option "<type name=\"Option.option\">%1</type>"
syntax function None "<const name=\"Option.option.None\">%t0</const>"
syntax function Some "<app><const name=\"Option.option.Some\"/>%1</app>"
end
theory map.Map
syntax type map "<fun>%1%2</fun>"
syntax function get "<app>%1%2</app>"
syntax function ([]) "<app>%1%2</app>"
syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function const "<app><const name=\"_type_constraint_\"><fun>%t0%t0</fun></const><abs name=\"\"><type name=\"dummy\"/>%1</abs></app>"
end
theory set.SetGen
syntax predicate (==) "<app><const name=\"HOL.eq\"/>%1%2</app>"
syntax predicate subset "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
end
theory set.Fset
syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle-realize"
filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle"
filename "%f_%t_%g.xml"
transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
(* Why driver for MetiTarski *)
(* main author: Piotr Trojanek <piotr.trojanek@gmail.com> *)
(* TODO:
* real.FromInt
......
......@@ -37,6 +37,19 @@ theory list.List
syntax function Cons "((%1) :: (%2))"
end
theory list.Length
syntax function length "(List.length (%1))"
end
theory list.Append
syntax function (++) "(List.append (%1) (%2))"
end
theory list.Reverse
syntax function reverse "(List.rev (%1))"
end
(* WhyML *)
......
......@@ -109,7 +109,6 @@ theory int.MinMax
end
theory real.Real
syntax function zero "0"