Commit e6023da8 authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap

parent 93b3d87b
......@@ -8,7 +8,7 @@
particulier la solution avec les types classes qui reste a
implanter
* paper on the proof management system
* DONE paper on the proof management system
* DONE Encodings and transformations (Andrei+Francois FroCos 11)
* DONE Why presentation at the IVL workshop of CADE:
......@@ -72,39 +72,10 @@
** support de Yices 2 ? interesserait Cesar
==================== Roadmap for release 0.81 ========================
scheduled on March 2013
==================== Roadmap for release 0.82 ========================
== New Features to announce ==
o [logic] accept type expressions in clone substitutions
o [whyml] support for relation chains (e.g., "e1 = e2 < e3")
* [whyml] every exception raised in a function must be listed
in as "raises { ... }" clause. A postcondition may be omitted
and equals to "true" by default.
* [whyml] if a function definition contains a "writes { ... }"
clause, then every write effect must be listed. If a function
definition contains a "reads { ... }" clause, then every read
_and_ write effect must be listed.
* [drivers] syntax rules, metas, and preludes are inherited
through cloning. Keyword "cloned" becomes unnecessary and
is not accepted anymore.
o [why3ide] allow several files on the command-line
o [ocaml API] incompatible changes in Set/Map/Hashtbl modules
o [ocaml API] examples in the manual extended to API for Why3ml programs
o [stdlib] fixed inconsistency in map.MapPermut theory
o [prover] fixed Coq 8.4 support for theory real.Trigonometry
o [prover] support for Gappa up to 0.16.6
o [prover] support for Z3 4.2, 4.3.*
o [prover] support for Alt-Ergo 0.95.1
o [prover] support for CVC4
o [prover] support for PVS 6
o [prover] experimental support for mathematica
o [prover] experimental support for MathSAT5
o [examples] several new examples, including solutions to the
VerifyThis@fm2012 challenges
== Final preparation ==
* faire une passe sur le BTS
......@@ -112,41 +83,41 @@ scheduled on March 2013
* check that nightly bench is OK
* check that "make xml-validate" is OK
(see below : copy the dtd on the web)
* put 0.81 in file Version
* 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"
* test distrib/why3-0.81.tar.gz
* 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
~filliatr/ARCHIVE/www/why)
* put on the web page
- why3-0.81.tar.gz
cp distrib/why3-0.81.tar.gz /users/www-perso/projets/why3/download
- why3-0.82.tar.gz
cp distrib/why3-0.82.tar.gz /users/www-perso/projets/why3/download
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.81.pdf
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.82.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.81
cp -r doc/html /users/www-perso/projets/why3/doc-0.82
- 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.81
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.82
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.81 \
ln -s /users/www-perso/projets/why3/stdlib-0.82 \
/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.81
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.82
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.81 \
ln -s /users/www-perso/projets/why3/api-0.82 \
/users/www-perso/projets/why3/api
PROBLEME avec style.css
- update the main HTML page (sources are in repository why3-www)
......@@ -161,9 +132,9 @@ scheduled on March 2013
chmod -R g+w /users/www-perso/projets/why3
* make a last commit:
- git commit -m "release 0.81"
- add tag 0.81 to the git repository, using
git tag 0.81
- git commit -m "release 0.82"
- add tag 0.82 to the git repository, using
git tag 0.82
- do not forget to push it using
git push
git push --tags
......@@ -231,10 +202,126 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build theories, apply
- (CLAUDE) complete api.tex: explain how to build apply
transformations, write new functions on terms (A)
==================== Roadmap for release 0.81 ========================
released on March 25th, 2013
== New Features to announce ==
o [logic] accept type expressions in clone substitutions
o [whyml] support for relation chains (e.g., "e1 = e2 < e3")
* [whyml] every exception raised in a function must be listed
in as "raises { ... }" clause. A postcondition may be omitted
and equals to "true" by default.
* [whyml] if a function definition contains a "writes { ... }"
clause, then every write effect must be listed. If a function
definition contains a "reads { ... }" clause, then every read
_and_ write effect must be listed.
* [drivers] syntax rules, metas, and preludes are inherited
through cloning. Keyword "cloned" becomes unnecessary and
is not accepted anymore.
o [why3ide] allow several files on the command-line
o [ocaml API] incompatible changes in Set/Map/Hashtbl modules
o [ocaml API] examples in the manual extended to API for Why3ml programs
o [stdlib] fixed inconsistency in map.MapPermut theory
o [prover] fixed Coq 8.4 support for theory real.Trigonometry
o [prover] support for Gappa up to 0.16.6
o [prover] support for Z3 4.2, 4.3.*
o [prover] support for Alt-Ergo 0.95.1
o [prover] support for CVC4
o [prover] support for PVS 6
o [prover] experimental support for mathematica
o [prover] experimental support for MathSAT5
o [examples] several new examples, including solutions to the
VerifyThis@fm2012 challenges
== Final preparation ==
* 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
(see below : copy the dtd on the web)
* put 0.81 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"
* test distrib/why3-0.81.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.81.tar.gz
cp distrib/why3-0.81.tar.gz /users/www-perso/projets/why3/download
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.81.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.81
- 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.81
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.81 \
/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.81
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.81 \
/users/www-perso/projets/why3/api
PROBLEME avec style.css
- 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.81"
- add tag 0.81 to the git repository, using
git tag 0.81
- 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 ==
* extraction vers Caml
- PRIORITAIRE, JCF, ANDREI
* Documentation
- (CLAUDE) complete api.tex: explain how to build theories
==================== Roadmap for release 0.80 ========================
Change in programs' input syntax deserves incrementing version to 0.80
......
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