Mentions légales du service
Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container registry
Monitor
Service Desk
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Why3
why3
Commits
80dea17f
Commit
80dea17f
authored
13 years ago
by
MARCHE Claude
Browse files
Options
Downloads
Patches
Plain Diff
Roadmap updated, towards release 0.72
parent
f840e0be
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
ROADMAP
+33
-25
33 additions, 25 deletions
ROADMAP
doc/manpages.tex
+1
-1
1 addition, 1 deletion
doc/manpages.tex
with
34 additions
and
26 deletions
ROADMAP
+
33
−
25
View file @
80dea17f
...
...
@@ -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
...
...
This diff is collapsed.
Click to expand it.
doc/manpages.tex
+
1
−
1
View file @
80dea17f
...
...
@@ -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.
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment