diff --git a/ROADMAP b/ROADMAP index 6cee28e034cabd2f4d3f050f196f18e8813cfc47..22e336110c7c09785e9363f39df3b37f644e4eea 100644 --- a/ROADMAP +++ b/ROADMAP @@ -85,6 +85,28 @@ - also: BTS 13736 https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 + - (ANDREI) make the glossary available + + +* detect editors +*** check if coqide and also emacs/proof-general is installed + +* deplacer option -bench de why3replayer dans une commande de why3session + +* IDE +** todo: run detection immediately at start up if conf file absent or + outdated. should become doable with the new Session module +** "detect provers" menu +** syntax highlighting bugs ? + some keywords are not colored in the bottom-right window + (but they are in the top-right window) + NEED FEEDBACK which ones ??? + +* (JCF) reject global "val"s in typing environment for logic decls. + +* (CLAUDE) complete api.tex: explain how to build theories, apply + transformations, write new functions on terms (A) + ==================== Roadmap for release 0.72 ======================== @@ -120,7 +142,7 @@ See manual Section xx - add tag 0.72 to the git repository (do not forget to push it) * put on the web page - why3-0.72.tar.gz - - standard library online, using why3doc (make stdlibdoc) + - standard library online, using why3doc (make stdlibdoc), to http://why3.lri.fr/stdlib/ - API doc, produced using ocamldoc (make apidoc), to http://why3.lri.fr/api/ Note: check that URL of API doc is correct in doc/api.tex line 9. - update the main HTML page (sources are in why3-papers/www) @@ -161,6 +183,9 @@ See manual Section xx manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter} + - (ANDREI) complete technical.tex: section "Drivers of external + provers" + - DONE (GUILLAUME) Realisations Coq, comment fait l'utilisateur pour faire ses realisations ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié @@ -189,33 +214,23 @@ See manual Section xx "timelimit" en fait c'était déjà le cas - - (WHO?) complete api.tex: explain how to build theories, apply - transformations, write new functions on terms (A) - - - (ANDREI?) complete manpages.tex: section "Drivers of external - provers" - - - (WHO?) make the glossary available - * DONE permettre d'utiliser emacs/proof general a la place de coqide depuis why3ide -** partially done: -*** check if coqide resp emacs is installed -*** allow to choose which one the IDE Preferences +*** DONE allow to choose which one the IDE Preferences * (CLAUDE) why3session - - deplacer option -bench de why3replayer dans une commande de why3session - - passe sur la documentation ecrite par Francois reecrite par Guillaume + - DONE passe sur la documentation ecrite par Francois reecrite par Guillaume - DONE "why3replayer -latex" remplacé par "why3session latex" - DONE "why3html" remplacé par "why3session html" - DONE "why3stats" (src/ide/stats.ml) remplacé par "why3session info --stats" * (JCF) ameliorer why3doc - - rajouter la production des liens + - DONE rajouter la production des liens + - produire un index.html - entree makefile pour produire la bibliotheque standard de Why3 en HTML (pour mettre sur le site Web) -* provers +* DONE provers - DONE (CLAUDE) Ensure that we kill a prover after some time (ressurect %T ? with a meaning like twice the value of %t ?), because we cannot be sure they always honor their own -timeout @@ -225,21 +240,14 @@ See manual Section xx enumeration types (Alt-Ergo >= 0.94) => at least two drivers for Alt-Ergo, depending on its version number -* fix bugs and update the BTS - - (JCF) reject global "val"s in typing environment for logic decls. +* DONE fix bugs and update the BTS - DONE (CLAUDE) Refreshing the IDE pane for prover output -* (CLAUDE) IDE: +* DONE (CLAUDE) IDE: - DONE enlarge font (menu + shortcut Ctrl-+) - DONE Ctrl-A to select all rows - DONE Do not save if not needed - DONE ne pas ecrire saving sessions si on ne sauve pas la session - + todo: run detection immediately at start up if conf file absent or - outdated. should become doable with the new Session module - - syntax highlighting bugs ? - some keywords are not colored in the bottom-right window - (but they are in the top-right window) - NEED FEEDBACK which ones ??? - DONE add a scrollbar for the left panel * DONE (FRANCOIS) move Session module and its dependencies into the diff --git a/doc/manpages.tex b/doc/manpages.tex index 1b08ae4ef46ee78a788b2f6389de4748c1375575..2343a029356d25b57af1c680f9bd68171df033f8 100644 --- a/doc/manpages.tex +++ b/doc/manpages.tex @@ -12,7 +12,7 @@ provided by the \why environment. These are as follows: \item[\texttt{why3ml}] as \texttt{why3} but reads \why{} ML programs instead \item[\texttt{why3replayer}] replay the proofs stored in a session, for regression test purposes -\item[\texttt{why3bench}] produces benchmarks \todo{obsolete ?} +\item[\texttt{why3bench}] produces benchmarks. \item[\texttt{why3session}] dumps various informations from a proof session, and possibly modifies the session. \item[\texttt{why3doc}] produces HTML versions of \why source codes.