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 ?