Commit 70f184d4 authored by MARCHE Claude's avatar MARCHE Claude

option --to-known-prover disabled because not coherent with

the new system of uninstalled prover policies
Also updated roadmap: explicitate the \todo of the doc
parent 5c8cba5a
......@@ -147,6 +147,18 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* Documentation
- traiter les \todo :
install.tex:179:% \todo{que devient l'option -to-known-prover de why3session ?
manpages.tex:790:% \todo{A adapter en fonction de la decision sur l'upgrade de prover}
library.tex:8:\todo{Plutot la version produite avec why3doc}
library.tex:42:\section{Library \texttt{int}} \todo{Completer}
library.tex:120:\section{Library \texttt{array}} \todo{Mettre a jour}
library.tex:224:\section{Library \texttt{string}} \todo{Detailler}
manpages.tex:15:\item[\texttt{why3bench}] produces benchmarks \todo{obsolete ?}
manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter}
- (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é
......@@ -183,7 +195,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- (WHO?) make the glossary available
* permettre d'utiliser emacs/proof general a la place de coqide depuis
* DONE permettre d'utiliser emacs/proof general a la place de coqide depuis
why3ide
** partially done:
*** check if coqide resp emacs is installed
......
......@@ -21,7 +21,7 @@ configuration phase which is run as
This analyzes your current configuration and checks if requirements hold.
Compilation requires:
\begin{itemize}
\item The Objective Caml compiler, version \todo{3.10} or higher. It is
\item The Objective Caml compiler, version 3.11.2 or higher. It is
available as a binary package for most Unix distributions. For
Debian-based Linux distributions, you can install the packages
\begin{verbatim}
......@@ -175,10 +175,12 @@ proof attempts in a fine-grain way, using filters, as detailed in
Section~\ref{sec:why3session}.
\todo{que devient l'option -to-known-prover de why3session ?
(d'ailleurs documenté en tant que --convert-unknown ??) Pourrait-on
permettre à why3session d'appliquer les choix d'association
vieux-prover/nouveau-prouveur stockés par l'IDE ?}
% pour l'instant on ne documente pas
% \todo{que devient l'option -to-known-prover de why3session ?
% (d'ailleurs documenté en tant que --convert-unknown ??) Pourrait-on
% permettre à why3session d'appliquer les choix d'association
% vieux-prover/nouveau-prouveur stockés par l'IDE ?}
%%% Local Variables:
%%% mode: latex
......
......@@ -786,19 +786,20 @@ corresponds to \verb|--filter-verified-goal --conservative| and
removes the proof attempts that are not verified but which correspond
to verified goals.
\todo{A adapter en fonction de la decision sur l'upgrade de prover}
If you just want to update one session with updated provers you can
use \verb|--convert-unknown| instead of the option \verb|--to-prover|.
\begin{verbatim}
why3session copy --convert-unknown
\end{verbatim}
For each proof attempt associated to an unknown prover (a prover not in
\verb|.why3.conf|) and not archived, it will try to find a known prover
with the same name. If it finds one, the proof attempt is copied to this
prover and the old proof is set to archived. The corresponding edited
files, if any, are copied and regenerated for the new prover An archived
proof is not replayed by why3replayer.
% pour l'instant on ne documente pas
% \todo{A adapter en fonction de la decision sur l'upgrade de prover}
% If you just want to update one session with updated provers you can
% use \verb|--convert-unknown| instead of the option \verb|--to-prover|.
% \begin{verbatim}
% why3session copy --convert-unknown
% \end{verbatim}
% For each proof attempt associated to an unknown prover (a prover not in
% \verb|.why3.conf|) and not archived, it will try to find a known prover
% with the same name. If it finds one, the proof attempt is copied to this
% prover and the old proof is set to archived. The corresponding edited
% files, if any, are copied and regenerated for the new prover An archived
% proof is not replayed by why3replayer.
......
......@@ -65,9 +65,11 @@ let spec =
" the proof is set to archive" ) ::
("--unset-archive", Arg.Unit unset_opt_archived,
" the proof is set to replayable" ) ::
(*
("--to-known-prover",
Arg.Set opt_to_known,
" convert the unknown provers to the most similar known prover.")::
*)
["--to-prover",
Arg.String (fun s -> opt_to_prover := Some (read_opt_prover s)),
" the proof is copied to this new prover";
......
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