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 ?