ROADMAP 1.7 KB
Newer Older
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
1 2 3 4 5

= Roadmap for December 2010 =

== Documentation ==

MARCHE Claude's avatar
MARCHE Claude committed
6
1 Introduction (TODO: a finir)
7 8 9
2 getting started (TODO: finir why3 batch)
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
MARCHE Claude's avatar
MARCHE Claude committed
10 11
** build a task (done)
** call a prover (done) 
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories: TODO
7 Manpages
7.1 done
7.2 done
7.3 todo ?
7.4 todo
7.5 todo ?
7.6 IDE (TODO, Claude)
7.7 why.conf (TODO ?)
7.8 drivers (TODO ?)
7.9 transformations (TODO)
8 API: Andrei + Francois
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
27 28 29 30 31

== IDE ==

(Claude)

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35
* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
36 37 38
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and 
   implemented accordingly
MARCHE Claude's avatar
MARCHE Claude committed
39
* add transf "inline goal" (TODO)
40
** not urgent
41 42
* add button "remove" (TODO: implement)
* add button "replay" (TODO: implement)
43
** semantics: replay obsolete proofs
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
44 45 46

== Misc ==

MARCHE Claude's avatar
MARCHE Claude committed
47 48 49 50
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
51
* TODO: licence pour les boomy icons
MARCHE Claude's avatar
MARCHE Claude committed
52

53 54
* option -version a tous les executables (TODO)
** + affichage dans l'IDE (done)
MARCHE Claude's avatar
MARCHE Claude committed
55
* Builtin arrays in provers (TODO: Francois)
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
59
* META for ocamlfind (Done)
MARCHE Claude's avatar
MARCHE Claude committed
60
* headers (done)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
61 62 63



MARCHE Claude's avatar
docs  
MARCHE Claude committed
64 65


MARCHE Claude's avatar
MARCHE Claude committed
66 67 68



MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
69 70
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
71
* WhyML (JC) 
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
72 73 74
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
claude  
MARCHE Claude committed
75
* Coq realizations of theories
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
76

MARCHE Claude's avatar
docs  
MARCHE Claude committed
77 78 79 80



= Papers to write =
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
81 82 83 84 85 86 87 88

* 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 ?