Commit 3e1158c2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

prepare for release 0.84

parent f45b8ae4
* marks an incompatible change * marks an incompatible change
version 0.84, September 1, 2014
===============================
tools tools
* file generated by "why3session html f.mlw" is now * file generated by "why3session html f.mlw" is now
"f/why3session.html" and not "f/f.html" "f/why3session.html" and not "f/f.html"
...@@ -11,9 +14,22 @@ tools ...@@ -11,9 +14,22 @@ tools
* other tools have been moved to why3 subcommands too: config, doc, ide, * other tools have been moved to why3 subcommands too: config, doc, ide,
session, wc; for local usage, the old commands are still available session, wc; for local usage, the old commands are still available
proof sessions
o session files are split in two parts: "why3session.xml" and
"why3shapes". The latter file contains the checksums and the shapes
for the goals. That second file is not strictly needed for
replaying a proof session, it is only useful when input programs
are modified, to track obsolete goals. If Why3 is compiled with
compression support (provided by ocamlzip library) then files for
shapes are compressed into why3shapes.gz.
library library
* renamed array.ArraySorted -> array.IntArraySorted * renamed array.ArraySorted -> array.IntArraySorted
array.ArraySorted is now generic, with type and order relation parameters array.ArraySorted is now generic, with type and order relation parameters
* reduced amount of "use export" in the standard library: theories
now only export the symbols they define. Users may need to insert more
"use import" in their theories (typically int.Int, option.Option,
list.List, etc.).
provers provers
* fixed Coq printer (former Coq proofs may have to be updated, by removing * fixed Coq printer (former Coq proofs may have to be updated, by removing
...@@ -21,6 +37,7 @@ provers ...@@ -21,6 +37,7 @@ provers
o support for Coq8.4pl4 o support for Coq8.4pl4
o support for Isabelle2014 o support for Isabelle2014
o support for CVC4 1.4 o support for CVC4 1.4
o updated support for TPTP TFA syntax (used by provers Beagle and Princess)
transformations transformations
o new transformation "compute_in_goal" that simplifies the goal, by o new transformation "compute_in_goal" that simplifies the goal, by
...@@ -98,7 +115,7 @@ version 0.82, December 12, 2013 ...@@ -98,7 +115,7 @@ version 0.82, December 12, 2013
o [fix] PVS: fixed configuration and installation process o [fix] PVS: fixed configuration and installation process
o [fix] Coq tactic: now loads dynamic plug-ins o [fix] Coq tactic: now loads dynamic plug-ins
o [fix] bug #15493: correct Coq output for polymorphic algebraic data types 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 * [fix] wish #15053: Remove proof time from "Goals proved by only one prover" section
of why3session info --stats of why3session info --stats
o [fix] bug #13736: why3ml was slow when there are many inclusions o [fix] bug #13736: why3ml was slow when there are many inclusions
o [fix] bug #16488: decimals in TPTP syntax o [fix] bug #16488: decimals in TPTP syntax
......
...@@ -138,7 +138,14 @@ and no epsilon ...@@ -138,7 +138,14 @@ and no epsilon
* detect editors * detect editors
*** check if coqide and also emacs/proof-general is installed *** check if coqide and also emacs/proof-general is installed
* documentation des nouvelles features higher-order
* 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
polymorphe.
==================== Roadmap for release 0.84 ======================== ==================== Roadmap for release 0.84 ========================
...@@ -148,24 +155,15 @@ and no epsilon ...@@ -148,24 +155,15 @@ and no epsilon
CVC4 1.4, yices2 (quantifiers ?) beagle ? driver TPTP TFA ? autres ? CVC4 1.4, yices2 (quantifiers ?) beagle ? driver TPTP TFA ? autres ?
* completer le fichier CHANGES * completer le fichier CHANGES
** nouvelle facon d'appeler les outils "why3 xxx ..." ** nouvelle facon d'appeler les outils "why3 xxx ..." DONE
** strategies de preuve ** strategies de preuve, NO for next release only
** transformation "compute_in_goal" ** transformation "compute_in_goal", DONE, but rewrite rules not documented
** support de nouveaux prouveurs ** support de nouveaux prouveurs, DONE
** nouvelle structure des fichiers de session et de shape (compatibilité) ** nouvelle structure des fichiers de session et de shape (compatibilité), DONE
** new examples ? ** new examples ? BOF
* ajouter dans les instructions de release ci-dessous la procedure de * ajouter dans les instructions de release ci-dessous la procedure de
fabrication du paquet opam fabrication du paquet opam DONE
* documentation des nouvelles features higher-order
* 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
polymorphe.
== New Features to announce == == New Features to announce ==
...@@ -173,23 +171,25 @@ See CHANGES ...@@ -173,23 +171,25 @@ See CHANGES
== Final preparation == == Final preparation ==
* inform Jerry James <loganjerry@gmail.com> so that he can test the
Fedora package
* faire une passe sur le BTS * faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed * do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK * check that nightly bench is OK
* check that "make xml-validate-local" is OK * check that "make xml-validate-local" is OK
(see below : copy the dtd on the web) (see below : copy the dtd on the web)
* put 0.84 in file Version * put 0.84 in file Version, and then run ./config.status
* check/update the content of the About dialog in src/ide/gconfig.ml * check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600 around lines 550-600
* check headers * check headers
* check the file CHANGES, add the release date * check the file CHANGES, add the release date
* manual in PDF: check that macro \todo is commented out * manual in PDF:
in ./macros.tex, and then "make doc" ** update the date in doc/manual.tex (near \whyversion{})
** check that macro \todo is commented out in doc/macros.tex
** and then "make doc"
(check that manual in HTML is also generated, doc/html/index.html) (check that manual in HTML is also generated, doc/html/index.html)
* do "make dist" * do "make dist"
* test distrib/why3-0.84.tar.gz * test distrib/why3-0.84.tar.gz
* 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 * install web page for why2 which includes an updated page for the
quick migration guide. (sources are in CVS repository quick migration guide. (sources are in CVS repository
~filliatr/ARCHIVE/www/why). ~filliatr/ARCHIVE/www/why).
...@@ -233,7 +233,7 @@ See CHANGES ...@@ -233,7 +233,7 @@ See CHANGES
* prepare for the OPAM package * prepare for the OPAM package
. update opam/url: url and checksum of why-0.84.tar.gz . update opam/url: url and checksum of why-0.84.tar.gz
(use "md5sum distrib/why3-0.84.tar.gz") (use "md5sum distrib/why3-0.84.tar.gz")
. update opam/descr if necessary . update opam/descr if necessary
. update opam/opam with correct dependencies and such . update opam/opam with correct dependencies and such
...@@ -256,7 +256,7 @@ See CHANGES ...@@ -256,7 +256,7 @@ See CHANGES
opam pin add why3 --kind=git <...>/why3/.git opam pin add why3 --kind=git <...>/why3/.git
(it runs "opam install why3") (it runs "opam install why3")
. with opam < 1.2: . with opam < 1.2:
- first step: have a local copy of opam-repository if not done yet, e.g.: - first step: have a local copy of opam-repository if not done yet, e.g.:
git clone git@github.com:claudemarche/opam-repository.git git clone git@github.com:claudemarche/opam-repository.git
...@@ -268,10 +268,10 @@ See CHANGES ...@@ -268,10 +268,10 @@ See CHANGES
git pull --ff-only opam master git pull --ff-only opam master
- second step: - second step:
opam repository add local ~/recherche/opam-repository opam repository add local ~/recherche/opam-repository
opam install why3 opam install why3
(* test it, e.g. (* test it, e.g.
cp example/quicksort.mlw ~/tmp cp example/quicksort.mlw ~/tmp
why3ide ~/tmp/quicksort.mlw *) why3ide ~/tmp/quicksort.mlw *)
opam remove why3 opam remove why3
...@@ -1351,8 +1351,3 @@ The main new features of interest in the GUI are ...@@ -1351,8 +1351,3 @@ The main new features of interest in the GUI are
Any question, remark or bug report concerning only Why3 should be done Any question, remark or bug report concerning only Why3 should be done
using the Why3 public discussion list and bug tracker. using the Why3 public discussion list and bug tracker.
# Why version # Why version
VERSION=0.83+git VERSION=0.84
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
%BEGIN LATEX %BEGIN LATEX
\begin{LARGE} \begin{LARGE}
%END LATEX %END LATEX
Version \whyversion{}, December 2013 Version \whyversion{}, September 2014
%BEGIN LATEX %BEGIN LATEX
\end{LARGE} \end{LARGE}
%END LATEX %END LATEX
......
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