Commit 5f70e95e authored by MARCHE Claude's avatar MARCHE Claude

roadmap

parent 8fb94597
......@@ -109,7 +109,7 @@
** support de Yices 2 ? interesserait Cesar
==================== Roadmap for release 0.91 ========================
==================== Roadmap for next releases ========================
HighOrd: Coq output and OCaml extraction should produce lambda's from lambda's
and no epsilon
......@@ -143,31 +143,103 @@ and no epsilon
== New Features to announce ==
= syntax =
See CHANGES
* new clause "diverges". Loops and recursive calls not annotated
with variants will generate a warning, unless the "diverges" clause is given
* clauses "reads" and "writes" now accept an empty set
* modified syntax for "abstract": abstract <spec> <expr> end
== 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.84 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.84.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). ADD a colon on new syntax for 0.84. Change Proval into Toccata
* put on the web page
- why3-0.84.tar.gz
cp distrib/why3-0.84.tar.gz /users/www-perso/projets/why3/download
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.84.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.84
- 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.84
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.84 \
/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.84
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.84 \
/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
= provers =
- 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)
* new version of prover: Coq 8.4pl3
* Coq 8.3 is no longer supported
* new version of prover: Gappa 1.1.0
* improved support for Isabelle2013-2
- make everything writeable for the group
chmod -R g+w /users/www-perso/projets/why3
= tools =
* make a last commit:
- git commit -m "release 0.84"
- add tag 0.84 to the git repository, using
git tag 0.84
- do not forget to push it using
git push
git push --tags
* why3replayer: renamed options -obsolete-only to --obsolete-only,
-smoke-detector to --smoke-detector, -force to --force
* 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
= fix =
* removed inconsistency in libraries map.MapPermut and array.ArrayPermut.
Note: names, definitions, and meaning of symbols "permut..." have been
modified. See http://why3.lri.fr/stdlib-0.83/array.mlw.html for details.
* fixed compilation bug with lablgtk 2.18
== TODOs ==
* 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.83 ========================
== New Features to announce ==
See CHANGES
== Final preparation ==
......@@ -252,26 +324,15 @@ and no epsilon
* DONE replayer: replay should be considered failed if new goals appeared.
* documentation des nouvelles features higher-order
* fix problems with installed scripts that are missing a proper executable right (mails Frederic Boulanger)
* DONE ? fix problems with installed scripts that are missing a proper executable right (mails Frederic Boulanger)
* Isabelle Support:
** fix the problem with why3_jedit script missing executable bit
** DONE ? fix the problem with why3_jedit script missing executable bit
** DONE add a documentation: start "isabelle why3_jedit" before why3ide, use "Close C-w" to signal the end of edit to why3"
* 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.
* extraction vers Caml
** DONE utiliser ZArith
* bug #15629
==================== Roadmap for release 0.82 ========================
Scheduled for 9 december 2013
......
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