ROADMAP 2.11 KB
Newer Older
MARCHE Claude's avatar
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)
MARCHE Claude's avatar
MARCHE Claude committed
28
** citation cruanes10 inexistent
29
8 API: Andrei + Francois
30
  (should we really add that in the doc ?)
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35

== IDE ==

(Claude)

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

== Misc ==

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

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



MARCHE Claude's avatar
docs  
MARCHE Claude committed
69 70


MARCHE Claude's avatar
MARCHE Claude committed
71 72 73



MARCHE Claude's avatar
MARCHE Claude committed
74 75
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
76
* WhyML (JC) 
MARCHE Claude's avatar
MARCHE Claude committed
77 78 79
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
MARCHE Claude committed
80
* Coq realizations of theories
MARCHE Claude's avatar
MARCHE Claude committed
81

MARCHE Claude's avatar
docs  
MARCHE Claude committed
82 83 84 85



= Papers to write =
MARCHE Claude's avatar
MARCHE Claude committed
86 87 88 89 90 91 92 93

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