ROADMAP

= Roadmap for December 2010 =

== Documentation ==

1 Introduction (TODO: a finir)
2 getting started (TODO: finir why3 batch)
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
** build a task (done)
** call a prover (done) 
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories: done, although quite sparse
7 Manpages
7.1 Compilation, Installation done
7.2 external provers done
7.3 why3config (TODO Francois)
7.4 why3 (todo François)
7.5 whyml todo ?
7.6 IDE (TODO, Claude)
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
8 API: Andrei + Francois

== IDE ==

(Claude)

* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and 
   implemented accordingly
* add transf "inline goal" (TODO)
** not urgent
* add button "remove" (TODO: implement)
* add button "replay" (TODO: implement)
** semantics: replay obsolete proofs

== Misc ==

* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
* TODO: licence pour les boomy icons

* option -version a tous les executables (TODO)
** + affichage dans l'IDE (done)
* Builtin arrays in provers (TODO: Francois)
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (Done)
* headers (done)








= Roadmap for 2011 =

* WhyML (JC) 
* Jessie3
* traceability
* Coq plugin
* Coq realizations of theories




= Papers to write =

* Encodings and transformations (Andrei+Francois, CADE 2011, deadline January 2011)
* Caml code ?
* logic language for talking to provers
** FOL + poly + alg + ind + rec ? + theories
* VACID-0
* system description (e.g. at CAD, TACAS)
* rapports recherche ?