ROADMAP 1.85 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
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
MARCHE Claude's avatar
MARCHE Claude committed
15
6 Standard lib of theories: done, although quite sparse
16
7 Manpages
17
18
19
20
21
7.1 Compilation, Installation done
7.2 external provers done
7.3 why3config (TODO Francois)
7.4 why3 (todo François)
7.5 whyml todo ?
22
7.6 IDE (TODO, Claude)
23
24
25
26
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
27
8 API: Andrei + Francois
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
28
29
30
31
32

== IDE ==

(Claude)

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

== Misc ==

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

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



MARCHE Claude's avatar
docs    
MARCHE Claude committed
65
66


MARCHE Claude's avatar
MARCHE Claude committed
67
68
69



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

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

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



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

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