Commit 8bfbf655 authored by MARCHE Claude's avatar MARCHE Claude

reorganized roadmap

parent 893110f2
=== Long-term Roadmap (see below for roadmap to next release) ===========
============ Long-term Roadmap (see below for roadmaps to next release) ===========
* Logic language
** support for higher-order logic
** rename andb, orb, xorb and notb into and, or, xor and not
* more libraries (theories and modules)
* A true Jessie3 front-end ?
* Why3ML
** Fast WP a la Leino
** assert qui ne donne pas une hypothese dans la suite -> "check"
also: in a black box
* traceability: Partially done
(Claude)
DONE: traceability des hyp comme path dans le prog (depuis
Frama-C en particulier)
afficher les explications dans les outils en ligne de
commande why3 et why3bench + le path
* Add more examples in the regression tests and in the proval gallery
** add all examples from the VSTTE 2012 competition (JCF, ANDREI)
* A literate programming tool for Why3 (JCF)
* Papers to write
== Papers to write ==
* DONE Encodings and transformations (Andrei+Francois)
* DONE Why presentation at the IVL workshop of CADE:
......@@ -35,133 +10,182 @@
deadline: May 1st
* Caml code ?
* logic language for talking to provers
** FOL + poly + alg + ind + rec ? + theories
- FOL + poly + alg + ind + rec ? + theories
* VACID-0
* system description (e.g. at CAD, TACAS)
* rapports recherche ?
* IDE:
** edition, navigation (partially done)
** reimplement "hide proved goals" feature
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
== stages ==
== stages ==
** M1. preuve d'un petit compilateur, pas de pb de lieur,
* M1. preuve d'un petit compilateur, pas de pb de lieur,
eventuellement outils pour les preuves par recurrence
a la Leino, + fct size automatique
** M2. Lieur en Why3, POPLmark challenge. vers
* M2. Lieur en Why3, POPLmark challenge. vers
un theorie et/ou un module réutilisable de lieurs
** (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
* (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
besoin du plugin Coq?
== new major features ==
* Logic language
- support for higher-order logic
- rename andb, orb, xorb and notb into and, or, xor and not
* more libraries (theories and modules)
* A true Jessie3 front-end
* Why3ML
- Fast WP a la Leino
- assert qui ne donne pas une hypothese dans la suite -> "check"
also: in a black box
* Add more examples in the regression tests and in the proval gallery
* A literate programming tool for Why3 (JCF)
* IDE:
- edition, navigation (partially done)
- saving session: add shortcut "ctrl-S", but beware of confusion with saving the input file
- reimplement "hide proved goals" feature
+ suggested solution: replace model + filter_model by a custom model
(JC + ?)
- restore provers detection in the middle of a session.
- commentaires dans les sessions, attachés a chaque ligne
=== release d'apres ==========================================
=========== Middle-term roadmap ==========================================
* PRIORITAIRE, JCF et ANDREI, clone de module
** demarche: ecrire une API avec smart constructors garantissant
- demarche: ecrire une API avec smart constructors garantissant
le bon typage, et clone sera en premier lieu un de ces constructors
** cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
- cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
containeurs pour Adacore et Claire
NON PRIORITAIRE ?
** regions : strong update
** ghost code
** logic symbols used in programs
- NON PRIORITAIRE ?
+ regions : strong update
+ ghost code
+ logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI
- PRIORITAIRE, JCF, ANDREI
* Coq plugin
* Coq output
** corriger l'incoherence, comprendre si on veut vraiment accepter
- corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** also: BTS 13736
- understand problems when large number of goals (cf D Mentré examples)
- also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
=== Roadmap for next release ========================
== Nouveautés importantes ==
==================== Roadmap for release 0.72 ========================
== New Features to annouce ==
* Realisation Coq
* tool why3session avec -latex, -html, -stats, etc
* Coq Realizations
* tool why3session with -latex, -html, -stats, etc
* tool why3doc
* several versions of the same prover
* Improved IDE: left scrollbar, font enlargement, etc.
* Support for several versions of the same prover
* Improved IDE:
- left scrollbar
- font enlargement
- what else ?
* what else ?
* see also the file CHANGES
== Final preparation ==
* check that nightly bench is OK
* put 0.72 in file Version
* increment the magic number in config (needed ???)
* check headers
* check the file CHANGES
* manual in PDF: check that macro \todo is commented out
in ./macros.tex
* do "make distrib"
* test the distrib why3-0.72.tar.gz
* make a last commit:
- add tag 0.72 to the git repository (do not forget to push it)
* put on the web page
- why3-0.72.tar.gz
- standard library online, using why3doc
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
Note: check that URL of API doc is correct in doc/api.tex line 9.
- update the main HTML page (where is the sources ?)
* produce the Why3 part of ProVal gallery ?
* 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 ==
TODOS:
* (JCF, ANDREI) add all examples from the VSTTE 2012 competition
* Documentation
** GM Realisations Coq, comment fait l'utilisateur pour faire ses realisations
- (GUILLAUME) Realisations Coq, comment fait l'utilisateur pour faire ses realisations
ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié
** ??? revoir documentation du smoke detector
** Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
** CLAUDE Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé
- (WHO?) revoir documentation du smoke detector
- (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
- (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé
ET LES METTRE AU POINT
*** ANDREI ajouter option a why3config pour ajouter association ident-executable
*** CLAUDE meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
** complete api.tex: explain how to build theories, apply
- (ANDREI) ajouter option a why3config pour ajouter association ident-executable
- (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
- (WHO?) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
** make the glossary available
- (ANDREI?) complete manpages.tex: section "Drivers of external provers"
- (WHO?) make the glossary available
* CM why3session
** passe sur la documentation ecrite par Francois reecrite par Guillaume
** option -latex et -html deplacé de why3replayer vers why3session
** reprendre une partie de src/ide/stats.ml, et virer executable why3stats
* (CLAUDE) why3session
- passe sur la documentation ecrite par Francois reecrite par Guillaume
- DONE option -latex deplacée de why3replayer vers why3session
- option -html deplacée de why3replayer vers why3session
- reprendre une partie de src/ide/stats.ml, et virer executable why3stats
* JCF renommer why3html en why3doc
** rajouter les liens
** mettre bibliotheque standard de Why3 en HTML, sur le site Web
* (JCF) renommer why3html en why3doc
- rajouter la production des liens
- mettre la bibliotheque standard de Why3 en HTML, sur le site Web
* provers
** CLAUDE Ensure that we kill a prover after some time (ressurect %T ? with a
- DONE (CLAUDE) Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
** ANDREI better use of Alt-Ergo's builtin theories: records, enumeration types
- (ANDREI) better use of Alt-Ergo's builtin theories: records, enumeration types
(Alt-Ergo >= 0.94) => at least two drivers for Alt-Ergo, depending on its
version number
* DONE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
** avoid also duplication of type like prover_data record
** do not include task and transf in the data type, so that
one can reload, and redetect provers
** session + session_ro -> session_data + session_dynamic
* fix bugs and update the BTS
- (JCF) reject global "val"s in typing environment for logic decls.
- (CLAUDE) Refreshing the IDE pane for prover output
* ALL fix bug and update the BTS
** reject global "val"s in typing environment for logic decls.
* CM IDE:
** DONE enlarge font (menu + shortcut Ctrl-+)
** Ctrl-A to select all rows
** commentaires dans les sessions, attachés a chaque ligne
** BTS: Refreshing the IDE pane for prover output
** Do not save if not needed
** ne pas ecrire saving sessions si on ne sauve pas la session
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
* do not save if no change was made
** restore provers detection in the middle of a session.
* (CLAUDE) IDE:
- DONE enlarge font (menu + shortcut Ctrl-+)
- Ctrl-A to select all rows
- DONE Do not save if not needed
- DONE ne pas ecrire saving sessions si on ne sauve pas la session
+ todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** syntax highlighting
- syntax highlighting bugs ?
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
** DONE add a scrollbar for the left panel
- DONE add a scrollbar for the left panel
* DONE (FRANCOIS) move Session module and its dependencies into the Why3 library
- but avoid duplication with session_ro
- avoid also duplication of type like prover_data record
- do not include task and transf in the data type, so that
one can reload, and redetect provers
- session + session_ro -> session_data + session_dynamic
=== Roadmap for release 0.71 ========================
======================= Roadmap for release 0.71 ========================
* DONE Final preparation:
** put on the web page
......
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