Commit 44a8424a authored by MARCHE Claude's avatar MARCHE Claude

roadmap for 0.82

parent c0fbdd9c
......@@ -2,6 +2,13 @@
============ Long-term Roadmap (see below for roadmaps to next release) ===========
== projects ==
* modules, raffinement, these de Leon
*
== Papers to write ==
* paper on the module system, its semantics, realizations, avec en
......@@ -72,16 +79,76 @@
** support de Yices 2 ? interesserait Cesar
==================== Roadmap for release 0.83 ========================
== TODOs ==
* extraction vers Caml
** utiliser ZArith
* replayer
** deplacer option -bench dans une commande de why3session
* terminaison
** generer une obligation de preuve de well-foundedness quand on utilise
un variant avec "with R" (une seule fois pour chaque R !)
** quand une definition logique recursive ne peut pas etre verifiee
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq tactic
** ajout de bases de hint
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** "detect provers" menu
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* bug 15629
==================== Roadmap for release 0.82 ========================
Scheduled for August 2013 ?
Scheduled for 31 october 2013
== New Features to announce ==
* provers:
** veriT 201310
** Alt-Ergo 0.95.2
** CVC4 1.1 & 1.2 (?)
** Coq 8.4pl2
** Metitarski
** gappa 1.0.0
** Metis
** Beagle, Princess
** SPASS 3.8 ?
** Yices 1.?.?
* --stats: changed (detailler, temps, distinction root et subgoals, CLAUDE)
--hist: TODO documenter (voir Alain ou Mohamed sur les graphes SMT)
* bug fix: leading zeros in decimal literals
* bug fix: PVS output, types are nonempty
* improved shape mecanism for session updates (see VSTTE'13 paper).
Compatibility with session files from version 0.81 and earlier is
assured.
* BTS 13736 fixed
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
** syntax highlighting bugs ?
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
FIXED: it was caused by the language file for alt-ergo superseding the one for why3
== Final preparation ==
* faire une passe sur le BTS
......@@ -157,59 +224,53 @@ Scheduled for August 2013 ?
== TODOs ==
* replayer
** deplacer option -bench dans une commande de why3session
* discriminate, mettre les bons arguments par defaut (ANDREI)
* extraction vers Caml
- PRIORITAIRE, JCF, ANDREI
* tester avant la release sur
** BWare
** Prouveur de Martin
** examples de Frama-C/Jessie et Krakatoa
* terminaison
** generer une obligation de preuve de well-foundedness quand on utilise
un variant avec "with R" (une seule fois pour chaque R !)
** quand une definition logique recursive ne peut pas etre verifiee
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq detection
* Coq detection (et PVS) (CLAUDE, champ supplementaire compile_support = yes dans le prover-detection-data)
** refuser de detecter Coq si on n'a pas compilé avec le support de Coq
(i.e. si Coq a ete installé apres)
* Coq tactic
** ajout de bases de hint
* Coq tactic (CLAUDE, GUILLAUME, JCF, ANDREI)
** bug Prod(_,_,_) -> traiter le cas
* efficiency issues
- 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
- prouveur de Martin
* Smoke detector and absurd: on pourrait mettre un label particulier
sur le "false" genéré par absurd, pour indiquer que c'est
intentionel que l'on veuille prouver false. Un tel cas pourrait etre
intentionel que l'on veuille prouver false. FAIT
Un tel cas pourrait etre
traité de facon speciale par le smoke detector avec option "deep",
pour eviter une fausse alarme.
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** "detect provers" menu
** syntax highlighting bugs ?
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
it is caused by the language file for alt-ergo superseding the one for why3
PAS FAIT
* faire le menage dans les transformations d'induction : _int _ty
_ty_lex, et DOCUMENTER
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
_ty_lex, FAIT et DOCUMENTER PAS FAIT
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) complete api.tex: explain how to build apply
transformations, write new functions on terms (A)
- (CLAUDE) complete api.tex: explain how to build/apply
transformations, write new functions on terms
- LEON: add a section "further reading"
* bug fix: 16454 (ne pas envoyer des triggers arithmetiques) (GUILLAUME)
* bug fix: 15652 (ghost code detection)
* support for new provers
** Alt-Ergo 0.95.2 DONE
** CVC4 1.2 TODO: pb avec les booleens
** Coq 8.4pl2 TODO: probleme tactique Why3 ???
** Metitarski TODO: improve it (CLAUDE, GUILLAUME)
** others ?
......
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