ROADMAP 1.48 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
7
8
9
1 Introduction (TODO: a finir)
2 Syntax, tutorial: JCF + Andrei3
3 IDE (Claude)
4 Standard lib of theories: TODO
MARCHE Claude's avatar
MARCHE Claude committed
10
* semantics:
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
11
* tutorial for API:
MARCHE Claude's avatar
MARCHE Claude committed
12
13
14
15
16
** build a task (done)
** call a prover (done) 
** apply a transformation (TODO)
** develop a new transformation (TODO)
* API: Andrei + Francois
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
17
18
19
20
21

== IDE ==

(Claude)

MARCHE Claude's avatar
MARCHE Claude committed
22
23
24
25
* database, session save and restore (done)
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
26
27
28
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and 
   implemented accordingly
MARCHE Claude's avatar
MARCHE Claude committed
29
* add transf "inline goal" (TODO)
30
** not urgent
MARCHE Claude's avatar
MARCHE Claude committed
31
32
* add button "remove" (TODO)
* add button "replay" (TODO)
33
** semantics: replay obsolete proofs
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
34
35
36

== Misc ==

MARCHE Claude's avatar
MARCHE Claude committed
37
38
39
40
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
41
* TODO: licence pour les boomy icons
MARCHE Claude's avatar
MARCHE Claude committed
42

43
44
* option -version a tous les executables (TODO)
** + affichage dans l'IDE (done)
MARCHE Claude's avatar
MARCHE Claude committed
45
* Builtin arrays in provers (TODO: Francois)
MARCHE Claude's avatar
MARCHE Claude committed
46
47
48
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
49
* META for ocamlfind (Done)
MARCHE Claude's avatar
MARCHE Claude committed
50
* headers (done)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
51
52
53



MARCHE Claude's avatar
docs    
MARCHE Claude committed
54
55


MARCHE Claude's avatar
MARCHE Claude committed
56
57
58



MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
59
60
= Roadmap for 2011 =

MARCHE Claude's avatar
MARCHE Claude committed
61
* WhyML (JC) 
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
62
63
64
* Jessie3
* traceability
* Coq plugin
MARCHE Claude's avatar
claude    
MARCHE Claude committed
65
* Coq realizations of theories
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
66

MARCHE Claude's avatar
docs    
MARCHE Claude committed
67
68
69
70



= Papers to write =
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
71
72
73
74
75
76
77
78

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