ROADMAP 2 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
2 getting started (Claude: done, to be read by others)
8 9
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
10 11
** build a task (Claude: done, to be read by others)
** call a prover (Claude: done, to be read by others) 
12 13 14
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
15 16
6 Standard lib of theories: 
  (Claude: done, although quite sparse, to be read by others)
17
7 Manpages
18 19
7.1 Compilation, Installation (done)
7.2 external provers (done)
20
7.3 why3config (TODO Francois)
21 22
7.4 why3 (TODO François)
7.5 whyml (TODO ?)
23
7.6 IDE (TODO, Claude)
24 25 26 27
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
28
8 API: Andrei + Francois
29
  (should we really add that in the doc ?)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
30 31 32 33 34

== IDE ==

(Claude)

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

== Misc ==

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

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



MARCHE Claude's avatar
docs  
MARCHE Claude committed
66 67


MARCHE Claude's avatar
MARCHE Claude committed
68 69 70



MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
71 72
= Roadmap for 2011 =

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

MARCHE Claude's avatar
docs  
MARCHE Claude committed
79 80 81 82



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

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