ROADMAP 2.11 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)
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
roadmap  
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
roadmap  
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
roadmap  
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
roadmap  
MARCHE Claude committed
74
75
= Roadmap for 2011 =

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

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



= Papers to write =
MARCHE Claude's avatar
roadmap  
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 ?