updated roadmap

parent adaf9119
= Roadmap for second release, as early as possible in 2011 =
* fix local installation
** fix local executables names (DONE)
* fix problems with .why.conf
** if we distribute the current state, users who already have a ~/.why.conf
will get a error message because of missing loadpath to modules
Done? - the magic number will force to not use the old ~/.why.conf of
the user
** generally speaking, we should rethink the design of that .why.conf: avoid
absolute paths,
Partially done - libdir, datadir, loadpath, ... are not written in why.conf
if they correspond to the default value.
* proof replay
** in IDE: replay all obsolete but previously successful proofs
** in whybench
** add replay of existing proofs in "make bench" to detect regression
** add automatic recompilation, install and bench every night on moloch
* IDE: implement "inline" (use transformation inline_goal)
** partially done
** problem 1: detect that transformation did nothing
* IDE: debug "hide proved goals" feature
* IDE: ajouter "invalid" comme cas de resultats de preuve
(utiliser call_provers.proof_result dans gmain)
* IDE, file names in DB: use only file names relative to the db file (DONE)
= Roadmap for 2011 =
= Roadmap for 2011 =========================================================
* WhyML (JC)
* Jessie3
* traceability
* Coq plugin
* Coq realizations of theories
* Coq realization of theories
* more libraries (theories and modules)
* IDE: edition, navigation
* HOL
* IDE: no more threads
* Papers to write
* Encodings and transformations (Andrei+Francois, CADE 2011,
deadline January 2011) DONE
* 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 ?
= Papers to write =
=== Roadmap for third release =================================================
* 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 ?
* proof replay
** in IDE: replay all obsolete but previously successful proofs
** in whybench
** add replay of existing proofs in "make bench" to detect regression
** add automatic recompilation, install and bench every night on moloch
* IDE: implement "inline" (use transformation inline_goal)
** partially done
** problem 1: detect that transformation did nothing
* IDE: debug "hide proved goals" feature
* IDE: ajouter "invalid" comme cas de resultats de preuve
(utiliser call_provers.proof_result dans gmain)
* IDE, file names in DB: use only file names relative to the db file (DONE)
=== Roadmap for second release, as early as possible in 2011 ================
* fix local installation
** fix local executables names (DONE)
* fix problems with .why.conf (DONE)
** if we distribute the current state, users who already have a ~/.why.conf
will get a error message because of missing loadpath to modules
Done? - the magic number will force to not use the old ~/.why.conf of
the user
** generally speaking, we should rethink the design of that .why.conf: avoid
absolute paths,
Partially done - libdir, datadir, loadpath, ... are not written in
why.conf if they correspond to the default value.
= Roadmap for December 2010 =
=== Roadmap for December 2010 ================================================
== Documentation ==
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment