ROADMAP

= Roadmap for December 2010 =

== Documentation ==

1 Introduction (TODO: a finir)
2 getting started (Claude: done, to be read by others)
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
** build a task (Claude: done, to be read by others)
** call a prover (Claude: done, to be read by others) 
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories: 
  (Claude: done, although quite sparse, to be read by others)
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)
** citation cruanes10 inexistent
8 API: Andrei + Francois
  (should we really add that in the doc ?)

== 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" 
** removing goals: done, but status need update
** removing transformation: (TODO: implement)
* add button "replay" (TODO, not urgent)
** 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 ?