Commit 72521ec5 authored by Clément Fumex's avatar Clément Fumex
Browse files

Merge branch 'master' into bv_rea_clem

Conflicts:
	examples/hackers-delight/why3session.xml
	examples/hackers-delight/why3shapes.gz
	theories/bv.why
parents 1a0d9e4a 37fa5ab1
* marks an incompatible change
Version 0.86.1, May 22, 2015
============================
IDE
o improved task highlighting for negated premises
(contributed by Mikhail Mandrykin, AstraVer project)
provers
o support for Gappa 1.2 (released May 19, 2015)
bug fixes
o why3doc: garbled output
version 0.86, May 11, 2015
==========================
core
o steps limit for reliable replay of proofs, available for Alt-Ergo
and CVC4
......@@ -27,16 +43,18 @@ provers
http://www.lix.polytechnique.fr/~lengrand/Psyche/)
o preliminary support for upcoming CVC4 1.5 (steps feature)
bug fixes:
o bug in interpreter in presence of nested mutable fields
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
IDE:
IDE
o config file not automatically saved anymore at exit. Configuration
is saved on disk for future sessions if, and only if, preferences
window is exited by hitting the "Save&Close" button
o right part of main window organized in tabs.
o better explanations and task highlighting
(contributed by Mikhail Mandrykin, AstraVer project)
bug fixes
o bug in interpreter in presence of nested mutable fields
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
version 0.85, September 17, 2014
================================
......
......@@ -147,6 +147,52 @@ and no epsilon
chaque instance necessaires. plutot qu'un seul symbole _match
polymorphe.
==================== Roadmap for release 0.87 ========================
DATE : ?
Release Notes (details in file CHANGES):
== TODO ==
* fix bug 18953 : (<>) not allowed as prefix form
* finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
* integrate server feature done by Johannes
* Coq realization of bitvector theory
* make counter-examples feature more robust
* support for both isabelle 2014 and 2015
* review support for division operators by SMT provers
* take some time to fix some bugs of the BTS: 18029 at least
* use the file generated by altgr-ergo to replay proofs edited by altgr-ergo
alt-ergo -replay <file>.agr
* make the strategy feature public and documented. Possibly generate
default stratregies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
prover-detection-data.conf to tell if they should be used in the strategies,
with which priority
2 possible default strategies
. favor use of many prover before splitting or increading timeout
. or, on the contrary, favor splitting
. or, favor timelimt increase...
==================== Roadmap for release 0.86 ========================
DATE : fin avril / début mai
......@@ -159,17 +205,19 @@ Release Notes (details in file CHANGES):
== TODO ==
* plusieurs drivers acceptés sur la ligne de commande (AP)
* clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
-> not anymore, but more cleaning can be done: no need to separate all theories in drivers for Z3 and CVC4, since the same theory can be put several times in a driver (or imported sub-drivers)
* decide if GUI with tabs is convenient enough
-> onglets dans why3 ide : est-ce apprécié ? OUI
mais enlever l'onglet "Counterexamples" avant la release
* for next release: complete realization of bitvector library
== DONE ==
* clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
-> not anymore, but more cleaning can be done: no need to separate all theories in drivers for Z3 and CVC4, since the same theory can be put several times in a driver (or imported sub-drivers)
* DONE plusieurs drivers acceptés sur la ligne de commande (AP)
* solve issues with metitarski
. DONE theory PowerReal
. DONE crashes when applied on a WP (see examples/my_cosine.mlw)
......@@ -216,15 +264,7 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
(check that manual in HTML is also generated, doc/html/index.html)
* do "make dist"
* test distrib/why3-0.86.tar.gz
* put on the web page why3-0.86.tar.gz:
cp distrib/why3-0.86.tar.gz /users/www-perso/projets/why3/download
* inform Jerry James <loganjerry@gmail.com> so that he can test the
Fedora package
* install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository
~filliatr/ARCHIVE/www/why).
* move distrib from Why3 site to Inria forge:
** remove /users/www-perso/projets/why3/download/why3-0.86.tar.gz
** upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* put on the web page
- the manual in PDF
......@@ -239,35 +279,19 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
make stdlibdoc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.86 \
/users/www-perso/projets/why3/stdlib
ln -s -n -f stdlib-0.86 /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.86
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.86 \
/users/www-perso/projets/why3/api
make apidoc
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
ln -s -n -f api-0.86 /users/www-perso/projets/why3/api
- update the main HTML page (sources are in repository why3-www)
edit index.html
edit index.html, change at least all occurrences of 0.85 by 0.86, and
update the url for download
make (to check validity)
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
* prepare for the OPAM package
. update opam/url: url and checksum of why-0.86.tar.gz
(use "md5sum distrib/why3-0.86.tar.gz")
. update opam/descr if necessary
. update opam/opam with correct dependencies and such
* make a last commit:
- git commit -am "release 0.86"
- add tag 0.86 to the git repository, using
......@@ -279,15 +303,11 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* The next commit : add +git to the version in file Version
* test the OPAM package
* prepare the OPAM package
. with opam 1.2:
opam pin add why3 --kind=git <...>/why3/.git
(it runs "opam install why3")
. with opam < 1.2:
- first step: have a local copy of opam-repository if not done yet, e.g.:
. obtain a local copy of opam repository, or obtain a former one :
git clone git@github.com:claudemarche/opam-repository.git
cd opam-repository/
......@@ -299,21 +319,25 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
git reset --hard opam/master
git push
- second step: copy why3 opam files into it :
. copy former files:
cd packages/why3
cp -r <source why3>/opam why3.0.86
cp -r packages/why3-base/why3-base-0.85 packages/why3-base/why3-base-0.86
cp -r packages/why3/why3-0.85 packages/why3/why3-0.86
- second step:
. update packages/why3-base/why3-base-0.86/url:
url and checksum of why-0.86.tar.gz obtained via
opam repository add local <...>/opam-repository
opam install why3
(* test it, e.g.
cp example/quicksort.mlw ~/tmp
why3 ide ~/tmp/quicksort.mlw *)
opam remove why3
opam repository remove local
md5sum distrib/why3-0.86.tar.gz
. update packages/why3-base/why3-base-0.86/descr if necessary
. update packages/why3/why3-0.86/descr if necessary
. update packages/why3-base/why3-base-0.86/opam with correct dependencies and such
. update packages/why3/why3-0.86/opam with correct dependencies and such
(at least the dependency on why3-base should be fixed)
* test the OPAM package (requires opam 1.2)
opam pin why3 ./.git
opam install why3
* make a pull request on OPAM
......@@ -322,12 +346,18 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
git push
sur github: creer un pull request
* inform Jerry James <loganjerry@gmail.com> so that he can produce the
Fedora package
* 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
(TODO: add the procedure here)
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
* Once the OPAM package is pulled in the main OPAM repository: a
nnounce the distrib
What to put in the announcement: see New Features above
==================== Roadmap for release 0.85 ========================
......
# Why version
VERSION=0.85+git
VERSION=0.86+git
......@@ -111,7 +111,7 @@ AC_ARG_ENABLE(doc,
enable_doc=yes)
AC_ARG_ENABLE(html-doc,
AS_HELP_STRING([--enable-html-doc], [do not build HTML documentation]),,
AS_HELP_STRING([--disable-html-doc], [do not build HTML documentation]),,
enable_html_doc=yes)
# Experimental Jessie3 Frama-C plugin, disabled by default
......@@ -171,8 +171,8 @@ OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION"
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.*|4.00.0)
AC_MSG_ERROR(You need Objective Caml 4.00.1 or higher);;
0.*|1.*|2.*|3.*|4.00.*)
AC_MSG_ERROR(You need Objective Caml 4.01.0 or higher);;
esac
# Ocaml library path
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, September 2014
Version \whyversion{}, May 2015
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -141,20 +141,20 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
\bigskip
%END LATEX
\textcopyright 2010-2014 University Paris-Sud, CNRS, Inria
\textcopyright 2010-2015 University Paris-Sud, CNRS, Inria
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
\urldef{\urlbware}{\url}{http://bware.lri.fr/}
\urldef{\urlproofinuse}{\url}{http://www.spark-2014.org/proofinuse}
This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
\urlutcat\end{latexonly}), the `\ahref{\urlhilite}{Hi-Lite}'
\urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
System@tic competitivity cluster, and the `\ahref{\urlbware}{BWare}'
System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
ANR project (ANR-12-INSE-0010\begin{latexonly},
\urlbware\end{latexonly}).
\urlbware\end{latexonly}) ; and the \ahref{\urlproofinuse}{Joint Laboratory ProofInUse} (ANR-13-LAB3-0007\begin{latexonly}, \urlproofinuse\end{latexonly})
\end{flushleft}
\end{center}
......@@ -265,7 +265,7 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
The syntax of \whyml programs changed in release 0.80.
The syntax of \whyml programs changed in release 0.80.
The table in Figure~\ref{fig:syntax080} summarizes the changes.
\begin{figure}[thbp]
......
......@@ -9,7 +9,7 @@ valid "Valid"
invalid "Invalid"
unknown "I don't know" ""
timeout "Timeout"
stepslimitexceeded "Steps limit reached"
steplimitexceeded "Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
......
......@@ -32,8 +32,8 @@ timeout "interrupted by timeout"
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -42,13 +42,4 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
......@@ -18,10 +18,13 @@ import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
(* temporarily disabled: too much experimental
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
......@@ -37,14 +40,18 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
stepslimitexceeded "??"
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
*)
(*
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -53,15 +60,6 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
import "cvc4_bv.gen"
......@@ -51,8 +51,10 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
stepslimitexceeded "??"
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
......
......@@ -29,6 +29,17 @@ transformation "simplify_formula"
transformation "encoding_smt"
transformation "encoding_sort"
(*
disabled: veriT seems more efficient with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
(*
Local Variables:
......
import "yices_bare.drv"
(* Why3 driver for Yices (SMT-like syntax) *)
prelude ";;; this is a prelude for Yices "
printer "yices"
filename "%f-%t-%g.ycs"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
import "discrimination.gen"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
(* could we do this? *)
(* meta "eliminate_algebraic" "keep_enums" *)
end
theory int.Int
prelude ";;; this is a prelude for Yices integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- 0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
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 ZeroLessOne
end
theory real.Real
prelude ";;; this is a prelude for Yices real arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
(* Yices division doesn't accept anything else than constant on
denominator so we don't use it (except for constant cf printer) *)
(* syntax function (/) "(/ %1 %2)" *)
syntax function (-_) "(- 0 %1)"
(* syntax function inv "(/ 1 %1)" *)
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
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 Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function notb "(not %1)"
end
theory map.Map
syntax type map "(-> %1 %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
syntax function get "(%1 %2)"
syntax function ([]) "(%1 %2)"
syntax function set "(update %1 (%2) %3)"
syntax function ([<-]) "(update %1 (%2) %3)"
meta "encoding : lskept" function const
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for Yices "
printer "yices"
filename "%f-%t-%g.ycs"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
(* could we do this? *)
(* meta "eliminate_algebraic" "keep_enums" *)
end
theory int.Int
prelude ";;; this is a prelude for Yices integer arithmetic"
syntax function zero "0"
syntax function one "1"