Commit e429a822 authored by MARCHE Claude's avatar MARCHE Claude

start of ide man page

parent 89435c10
......@@ -23,6 +23,7 @@
* Coq output (done)
* Gappa output (done)
* debug hide goals (TODO)
* add "context" options (TODO)
* add transf "inline goal" (TODO)
* add button "remove" (TODO)
* add button "replay" (TODO)
......@@ -34,6 +35,7 @@
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
* option -version a tous les executables + affichage dans l'IDE (TODO)
* Builtin arrays in provers (TODO: Francois)
* make install (done)
* make export (TODO: JCF)
......@@ -45,6 +47,9 @@
= Roadmap for 2011 =
* WhyML (JC)
......
......@@ -5,6 +5,10 @@
\section{IDE}
The graphical interface allows to browse into a file or a set of
files, and check the validity of goals with external provers, in a
friendly way. This section presents the basic use of this GUI. Please refer to Section~\ref{sec:ideref} for a more complete description.
\section{Other tools}
\begin{itemize}
......
......@@ -57,6 +57,46 @@ pour chaque prouveur: lien sur page why/prover tips.
\section{The \texttt{why3ml} tool}
\section{The \texttt{why3ide} tool}
\label{sec:ideref}
\subsection{Command-line options}
\begin{description}
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}
\subsection{Left toolbar}
\begin{description}
\item[Provers] To each detected prover corresponds to a button in this
prover framed box. Clicking on this button starts the prover on the
selected goal(s).
\item[Edit] Start an editor on the selected task.
For automatic provers, this allows to see the file sent to the
prover.
For interactive provers, this also allows to add or modify the
corresponding proof script. The modifications are saved, and can be
retrieved later even if the goal was modified.
\item[Split] This splits the current goal into subgoals if it is a
conjunction of two or more goals.
\end{description}
\subsection{Menus}
\begin{description}
\item[File/Detect provers]
\end{description}
\subsection{Preferences}
\subsection{Structure of the database file}
TODO
\section{The \texttt{why.conf} configuration file}
......
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