Commit d284bb83 authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap + doc install-lib

parent 60a08f6c
......@@ -4,27 +4,29 @@
== Documentation ==
1 Introduction (TODO: a finir)
2 getting started (TODO: finir why3 batch)
2 getting started (Claude: done, to be read by others)
3 Syntax, tutorial (TODO: JCF + Andrei)
4 tutorial for API:
** build a task (done)
** call a prover (done)
** build a task (Claude: done, to be read by others)
** call a prover (Claude: done, to be read by others)
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories: done, although quite sparse
6 Standard lib of theories:
(Claude: done, although quite sparse, to be read by others)
7 Manpages
7.1 Compilation, Installation done
7.2 external provers done
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 ?
7.4 why3 (TODO François)
7.5 whyml (TODO ?)
7.6 IDE (TODO, Claude)
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
8 API: Andrei + Francois
(should we really add that in the doc ?)
== IDE ==
......@@ -37,10 +39,9 @@
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and
implemented accordingly
* add transf "inline goal" (TODO)
** not urgent
* add transf "inline goal" (TODO, not urgent)
* add button "remove" (TODO: implement)
* add button "replay" (TODO: implement)
* add button "replay" (TODO, not urgent)
** semantics: replay obsolete proofs
== Misc ==
......@@ -57,7 +58,7 @@
* make install (done)
* make export (TODO: JCF)
* "make -j" (done)
* META for ocamlfind (Done)
* META for ocamlfind (done)
* headers (done)
......
......@@ -51,7 +51,11 @@ The Why3 executables are then available in subdirectory \texttt{bin/}.
\subsection{Installation of the Why3 library}
\label{sec:installlib}
TODO
By default, the Why3 library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
\section{Installation of external provers}
......@@ -169,9 +173,15 @@ used to provide other informations :
\section{The \texttt{why3ml} tool}
\section{The \texttt{why3ide} tool}
[TO BE COMPLETED]
\section{The \texttt{why3ide} GUI}
\label{sec:ideref}
The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.
\subsection{Command-line options}
\begin{description}
......
......@@ -210,7 +210,8 @@ hello_proof.why HelloProof G3 : Valid (0.01s)
\end{verbatim}
Finally, a transformation to apply to goals before proving them can be
specified. To know the unique identifier associated to transformations, do as follows.
specified. To know the unique identifier associated to
transformations, do as follows.
\begin{verbatim}
> why3 --list-transforms
Known non-splitting transformations:
......
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