Commit 272630ca authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Update doc

parent e9c93948
...@@ -74,6 +74,8 @@ ...@@ -74,6 +74,8 @@
** porter multirounding a jessie->Why3. Completer le mode full et faire passer ** porter multirounding a jessie->Why3. Completer le mode full et faire passer
interval_arith.c. Completer la galerie interval_arith.c. Completer la galerie
** preuve sur l'assembleur ** preuve sur l'assembleur
** support de Yices 2 ? interesserait Cesar
* extraction vers Caml * extraction vers Caml
- PRIORITAIRE, JCF, ANDREI - PRIORITAIRE, JCF, ANDREI
...@@ -112,13 +114,9 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 ...@@ -112,13 +114,9 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
(but they are in the top-right window) (but they are in the top-right window)
NEED FEEDBACK which ones ??? NEED FEEDBACK which ones ???
* (JCF) reject global "val"s in typing environment for logic decls.
* sessions * sessions
** mettre la dtd sur le web et changer l'entête des sessions pour qu'elles ** mettre la dtd sur le web et changer l'entête des sessions pour qu'elles
pointent dessus pointent dessus
** utiliser des chemins plus raisonnables pour indiquer la position des buts
dans les fichiers (e.g. relativement au fichier session ?)
==================== Roadmap for release 0.80 ======================== ==================== Roadmap for release 0.80 ========================
...@@ -207,6 +205,9 @@ Bug fixes: ...@@ -207,6 +205,9 @@ Bug fixes:
== TODOs == == TODOs ==
* (JCF) reject global "val"s in typing environment for logic decls.
* appliquer les changements de syntaxe des programmes dans la doc : aussi bien dans le tutorial que dans la BNF des manpages
* faire le menage dans les transformations d'induction : _int _ty * faire le menage dans les transformations d'induction : _int _ty
_ty_lex, et DOCUMENTER _ty_lex, et DOCUMENTER
...@@ -214,9 +215,7 @@ Bug fixes: ...@@ -214,9 +215,7 @@ Bug fixes:
* Sortie PVS * Sortie PVS
** avec mecanisme de realization ** avec mecanisme de realization
* support de Yices 2 ? interesserait Cesar * DONE mettre au propre les loc des fichiers de sessions, en particulier
* mettre au propre les loc des fichiers de sessions, en particulier
les noms de fichiers doivent etre relatifs au fichier de session les noms de fichiers doivent etre relatifs au fichier de session
lui-meme. Utiliser Sysutil.relativize_filename a bon escient. lui-meme. Utiliser Sysutil.relativize_filename a bon escient.
......
...@@ -6,7 +6,11 @@ ...@@ -6,7 +6,11 @@
\newcommand{\eg}{\emph{e.g.}\xspace} \newcommand{\eg}{\emph{e.g.}\xspace}
\newcommand{\ie}{\emph{i.e.}\xspace} \newcommand{\ie}{\emph{i.e.}\xspace}
\newcommand{\emptyitem}{\begin{latexonly}~\end{latexonly}} \newcommand{\emptyitem}{%
%BEGIN LATEX
~
%ENDLATEX
}
% BNF grammar % BNF grammar
\newcommand{\keyword}[1]{\texttt{#1}} \newcommand{\keyword}[1]{\texttt{#1}}
......
...@@ -228,7 +228,8 @@ contains the time taken and the state of the proof: ...@@ -228,7 +228,8 @@ contains the time taken and the state of the proof:
\item \texttt{Valid}: the task is valid according to the prover. The \item \texttt{Valid}: the task is valid according to the prover. The
goal is considered proved. goal is considered proved.
\item \texttt{Invalid}: the task is invalid. \item \texttt{Invalid}: the task is invalid.
\item \texttt{Timeout}: the prover exceeds the time or memory limit. \item \texttt{Timeout}: the prover exceeded the time limit.
\item \texttt{OufOfMemory}: the prover exceeded the memory limit.
\item \texttt{Unknown}: the prover can't determine if the task \item \texttt{Unknown}: the prover can't determine if the task
is valid; Some additional information can be provided. is valid; Some additional information can be provided.
\item \texttt{Failure}: the prover reports a failure. \item \texttt{Failure}: the prover reports a failure.
...@@ -239,14 +240,16 @@ contains the time taken and the state of the proof: ...@@ -239,14 +240,16 @@ contains the time taken and the state of the proof:
Additionally a proof attempt can have the following attribute: Additionally a proof attempt can have the following attribute:
\begin{itemize} \begin{itemize}
\item obsolete:\index{obsolete!proof attempt} the proof attempt has not been run in \item obsolete:\index{obsolete!proof attempt} the prover associated to
its current state. You'll need to replay the proof attempt, ie run that proof attempt has not been run on the current task, but on a
the prover with the current state of the proof attempt, in order to earlier version of that task. You need to replay the proof
update the answer of the prover and remove this attribute. attempt, \emph{i.e.} run the prover with the current task of the proof
attempt, in order to update the answer of the prover and remove this
attribute.
\item archived:\index{archived!proof attempt} the proof attempt is not useful \item archived:\index{archived!proof attempt} the proof attempt is not useful
anymore it is kept for history, no why3 tools will select it by anymore it is kept for history, no why3 tools will select it by
default. The section \ref{sec:uninstalledprovers} shows an example default. The section \ref{sec:uninstalledprovers} shows an example
of its utilization. of its usage.
\end{itemize} \end{itemize}
Generally proof attempt are marked obsolete just after Generally proof attempt are marked obsolete just after
...@@ -280,9 +283,12 @@ changed are marked obsolete. ...@@ -280,9 +283,12 @@ changed are marked obsolete.
button starts the corresponding prover on the selected goal(s). button starts the corresponding prover on the selected goal(s).
\item[Split] splits the current goal into subgoals if it is a \item[Split] splits the current goal into subgoals if it is a
conjunction of two or more goals. conjunction of two or more goals. It corresponds to the
\verb|split_goal_wp| transformation.
\item[Inline] replaces the head predicate symbol of the goal with its definition. \item[Inline] replaces the head predicate symbol of the goal with its
definition. It corresponds to the
\verb|inline_goal| transformation.
\item[Edit] starts an editor on the selected task. \item[Edit] starts an editor on the selected task.
...@@ -338,6 +344,11 @@ A copy of the tools already available in the left toolbar, plus: ...@@ -338,6 +344,11 @@ A copy of the tools already available in the left toolbar, plus:
\item[Mark as obsolete] marks all the proof as \item[Mark as obsolete] marks all the proof as
obsolete. obsolete.
This allows to replay every proofs. This allows to replay every proofs.
\item[Apply non-splitting transformation] apply one of the available
transformations, as listed in Section~\ref{sec:transformations}
\item[Apply non-splitting transformation]. Same as above, but for
splitting transformations, \emph{i.e.} those that can generated
several sub-goals.
\end{description} \end{description}
\item[Menu \textsf{Help}] \item[Menu \textsf{Help}]
...@@ -359,6 +370,9 @@ are groups together under several tabs ...@@ -359,6 +370,9 @@ are groups together under several tabs
\item the memory given to provers, in megabytes \item the memory given to provers, in megabytes
\item the maximal number of simultaneous provers allowed to run in parallel \item the maximal number of simultaneous provers allowed to run in parallel
\end{itemize} \end{itemize}
By default, modification of any of these settings has effect only
for the current run of the GUI. a checkbox allows you to save these
settings also for future sessions.
\item a few display settings: \item a few display settings:
\begin{itemize} \begin{itemize}
\item introduce premises: if selected, the goal of the task shown in \item introduce premises: if selected, the goal of the task shown in
...@@ -396,8 +410,9 @@ are groups together under several tabs ...@@ -396,8 +410,9 @@ are groups together under several tabs
the editor to use will be set to ``CoqIDE'' by default, and this the editor to use will be set to ``CoqIDE'' by default, and this
\urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/} \urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
dialog allows you to select the Emacs editor and its dialog allows you to select the Emacs editor and its
\ahref{\urlprfgen}{Proof General} mode instead% \todo{uncomment the following}
\begin{latexonly} (\urlprfgen)\end{latexonly}. % \ahref{\urlprfgen}{Proof General} mode instead%
% \begin{latexonly} (\urlprfgen)\end{latexonly}.
\end{itemize} \end{itemize}
\item[\textsf{Provers} tab] \item[\textsf{Provers} tab]
allows to select which of the installed provers one wants to see allows to select which of the installed provers one wants to see
...@@ -791,9 +806,9 @@ output. ...@@ -791,9 +806,9 @@ output.
cela soit coherent avec la sortie HTML ci-dessous} cela soit coherent avec la sortie HTML ci-dessous}
\begin{figure}[t] \begin{figure}[t]
\begin{center} \begin{center}
\begin{toimage} %HEVEA\begin{toimage}
\input{HelloProof.tex} \input{HelloProof.tex}
\end{toimage} %HEVEA\end{toimage}
%HEVEA\imageflush %HEVEA\imageflush
\end{center} \end{center}
\caption{LaTeX table produced for the HelloProof example (style 1)} \caption{LaTeX table produced for the HelloProof example (style 1)}
...@@ -802,9 +817,9 @@ output. ...@@ -802,9 +817,9 @@ output.
\begin{figure}[t] \begin{figure}[t]
\begin{center} \begin{center}
\begin{toimage} %HEVEA\begin{toimage}
\input{HelloProof-style2.tex} \input{HelloProof-style2.tex}
\end{toimage} %HEVEA\end{toimage}
%HEVEA\imageflush %HEVEA\imageflush
\end{center} \end{center}
\caption{LaTeX table produced for the HelloProof example (style 2)} \caption{LaTeX table produced for the HelloProof example (style 2)}
...@@ -824,21 +839,22 @@ There are three styles of output: `table', `simpletree', and ...@@ -824,21 +839,22 @@ There are three styles of output: `table', `simpletree', and
\begin{figure}[t] \begin{figure}[t]
\begin{center} \begin{center}
\begin{latexonly} %BEGIN LATEX
\fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}} \fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}}
\end{latexonly} %END LATEX
\begin{htmlonly} \todo{uncomment the following}
\begin{rawhtml} % \begin{htmlonly}
<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr> % \begin{rawhtml}
<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr> % <table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr> % <td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr> % <td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.49</td><td bgcolor="#FF8000">0.00</td></tr> % <tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
<tr><td bgcolor="#C0FFC0" colspan="1">G2.2</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr> % <td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.49</td><td bgcolor="#FF8000">0.00</td></tr>
<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr> % <tr><td bgcolor="#C0FFC0" colspan="1">G2.2</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
</table> % <td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
\end{rawhtml} % </table>
\end{htmlonly} % \end{rawhtml}
% \end{htmlonly}
\end{center} \end{center}
\caption{HTML table produced for the HelloProof example} \caption{HTML table produced for the HelloProof example}
\label{fig:html} \label{fig:html}
......
...@@ -13,10 +13,15 @@ ...@@ -13,10 +13,15 @@
\usepackage{lmodern} \usepackage{lmodern}
%\usepackage{url} %\usepackage{url}
\usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref} \usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
%BEGIN LATEX
\usepackage{graphicx} \usepackage{graphicx}
%END LATEX
%HEVEA \newcommand{\includegraphics}[2][2]{\imgsrc{#2}}
\usepackage{listings} \usepackage{listings}
\usepackage{xspace} \usepackage{xspace}
\usepackage{hevea} %\usepackage{hevea}
%BEGIN LATEX %BEGIN LATEX
\setulmarginsandblock{30mm}{30mm}{*} \setulmarginsandblock{30mm}{30mm}{*}
...@@ -71,12 +76,12 @@ ...@@ -71,12 +76,12 @@
\vfill \vfill
\begin{latexonly} {
{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform} %BEGIN LATEX
\end{latexonly} \fontsize{40}{40pt}\selectfont
\begin{htmlonly} %END LATEX
{\Huge\bfseries\sffamily The Why3 platform} %HEVEA \Huge
\end{htmlonly} \bfseries\sffamily The Why3 platform}
\vfill \vfill
...@@ -120,20 +125,21 @@ $^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\ ...@@ -120,20 +125,21 @@ $^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120 $^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
\end{tabular} \end{tabular}
\begin{latexonly} %BEGIN LATEX
\bigskip \bigskip
\end{latexonly} %END LATEX
\textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria \textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat} \urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/} \urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}' \todo{uncomment the following}
national ANR project (ANR-08-SEGI-021-08\begin{latexonly}, % This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
\urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}' % national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the % \urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}'
System@tic competitivity cluster. % \begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
% System@tic competitivity cluster.
\end{flushleft} \end{flushleft}
\end{center} \end{center}
...@@ -238,9 +244,9 @@ are the following. ...@@ -238,9 +244,9 @@ are the following.
\cleardoublepage \cleardoublepage
\begin{latexonly} %BEGIN LATEX
\tableofcontents \tableofcontents
\end{latexonly} %END LATEX
%\input{intro.tex} %\input{intro.tex}
......
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