Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
125
Issues
125
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
85a04de5
Commit
85a04de5
authored
Aug 24, 2012
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
improved index
parent
c099ef7c
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
34 additions
and
26 deletions
+34
-26
doc/glossary.tex
doc/glossary.tex
+1
-1
doc/install.tex
doc/install.tex
+2
-2
doc/manpages.tex
doc/manpages.tex
+20
-17
doc/manual.tex
doc/manual.tex
+9
-4
doc/starting.tex
doc/starting.tex
+2
-2
No files found.
doc/glossary.tex
View file @
85a04de5
\newcommand
{
\why
}{
\textsc
{
Why
}}
%
\newcommand{\why}{\textsc{Why}}
\newglossaryentry
{
ident
}{
name=
{
identifier
}
,
...
...
doc/install.tex
View file @
85a04de5
...
...
@@ -153,10 +153,10 @@ with the GUI, and replay the proofs, you will be asked to choose
between
3
options:
\begin
{
itemize
}
\item
Keep the former proofs as they are. They will be marked as
``archived''
\index
{
archived
}
.
``archived''.
\item
Upgrade the former proofs to an installed prover
(
typically a
upgraded version
)
. The corresponding proof attempts will become
attached to this new prover, and marked as obsolete
\index
{
obsolete
}
,
attached to this new prover, and marked as obsolete,
to make their replay mandatory.
\item
Copy the former proofs to an installed prover. This is a
combination of the actions above: each proof attempt is duplicated,
...
...
doc/manpages.tex
View file @
85a04de5
...
...
@@ -210,17 +210,17 @@ contains the time taken and the state of the proof:
Additionally a proof attempt can have the following attribute:
\begin{itemize}
\item
obsolete:
\index
{
obsolete
}
the proof attempt has not been run in
\item
obsolete:
\index
{
obsolete
!proof attempt
}
the proof attempt has not been run in
its current state. You'll need to replay the proof attempt, ie run
the prover with the current state of the proof attempt, in order to
update the answer of the prover and remove this attribute.
\item
archived:
\index
{
archived
}
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
default. The section
\ref
{
sec:uninstalledprovers
}
shows an example
of its utilization.
\end{itemize}
Generally proof attempt are marked obsolete
\index
{
obsolete
}
just after
Generally proof attempt are marked obsolete just after
the start of why3ide. Indeed when you load a session in order to
modify it (not with
\texttt
{
why3session info
}
for instance), why3
rebuilds the goals to prove by using the information provided in the
...
...
@@ -228,8 +228,11 @@ session. If you modify the original file (.why, .mlw) or if the
transformations have changed (new version of why3) why3 will detect
that. The provers will perhaps answer differently on this new
problems. So the proof attempts that corresponds to a goal that
changed are marked obsolete. We say that a session is obsolete if new
goals are made obsolete by this method during start-up.
changed are marked obsolete.
% non
% We say that a session is obsolete if new
% goals are made obsolete by this method during start-up.
% Claude: Alors la je ne vois pas pourquoi
% A session can
...
...
@@ -263,7 +266,7 @@ goals are made obsolete by this method during start-up.
corresponding proof script. The modifications are saved, and can be
retrieved later even if the goal was modified.
\item
[Replay]
Replay all obsolete
\index
{
obsolete
}
proofs
\item
[Replay]
Replay all obsolete proofs
If ``only unproved goals'' is selected, only formerly successful
proofs are rerun. If ``all goals'', then all obsolete proofs are
...
...
@@ -306,7 +309,7 @@ goals are made obsolete by this method during start-up.
A copy of the tools already available in the left toolbar, plus:
\begin{description}
\item
[Mark as obsolete]
marks all the proof as
obsolete
\index
{
obsolete
}
.
obsolete.
This allows to replay every proofs.
\end{description}
...
...
@@ -477,8 +480,8 @@ file is fully proved, the subtree is not shown.
\paragraph
{
Obsolete proofs
}
When some proofs stored in the session file are
obsolete
\index
{
obsolete
}
,
When some proof
attempt
s stored in the session file are
obsolete
\index
{
obsolete
!proof attempt
}
,
the replay is run anyway, as with the replay button in the IDE. Then, the session
file will be updated if both
\begin{itemize}
...
...
@@ -499,7 +502,7 @@ option \verb|-force| described below.
\item
Option
\verb
|
-force
|
enforces saving the session, if all proof
attempts replayed correctly, even if some goals are not proved.
\item
Option
\verb
|
-obsolete-only
|
replays the proofs only if the session
is obsolete
\index
{
obsolete
}
.
contains obsolete proof attempts
.
\item
Option
\texttt
{
-smoke-detector
\{
none|top|deep
\}
}
tries to detect
if the context is self-contradicting.
\end{itemize}
...
...
@@ -569,14 +572,14 @@ The available commands are the following:
\item
[\texttt{mod}]
modifies some of the proofs, selected by a filter.
\item
[\texttt{copy}]
duplicates some of the proofs, selected by a filter.
\item
[\texttt{copy-archive}]
same as copy but also archives the
original proofs
\index
{
archived
}
.
original proofs
\index
{
archived
!proof attempt
}
.
\item
[\texttt{rm}]
remove some of the proofs, selected by a filter.
\end{description}
The first three commands do not modify the sessions, whereas the four
last modify them. Only the proof attempts recorded are modified. No
prover is called on the modified or created proof attempts, and
consequently the proof status is always marked as obsolete
\index
{
obsolete
}
.
consequently the proof status is always marked as obsolete.
All the commands above share the following common set of options:
common options:
...
...
@@ -629,13 +632,13 @@ The hierarchical structure of the session is printed as a tree in
ASCII. The files, theories, goals are marked with a question mark
\verb
|
?
|
, if they are not verified. A proof is usually said to be
verified if the proof result is
\verb
|
valid
|
and the proof is not
obsolete
\index
{
obsolete
}
.
obsolete.
However here specially we separate these two properties. On
the one hand if the proof suffers from an internal failure we mark it
with an exclamation mark
\verb
|
!
|
, otherwise if it is not valid we
mark it with a question mark
\verb
|
?
|
, finally if it is valid we add
nothing. On the other hand if the proof is obsolete we mark it with an
\verb
|
O
|
and if it is archived
\index
{
archived
}
we mark it with an
\verb
|
A
|
.
\verb
|
O
|
and if it is archived we mark it with an
\verb
|
A
|
.
For example, here are the session tree produced on the ``hello
proof'' example of Section~
\ref
{
chap:starting
}
.
...
...
@@ -818,14 +821,14 @@ attempts to work on:
provers. If this option is not specified, the proof are simply not
filtered by there corresponding prover.
\item
Option
\verb
|
--filter-verified yes
|
restricts the selection to
the proofs that are valid and not obsolete
s
. On contrary the option
the proofs that are valid and not obsolete. On contrary the option
\verb
|
--filter-verified no
|
select the ones that are not verified.
\verb
|
--filter-verified all
|
, the default, does not select on this property.
\item
Option
\verb
|
--filter-verified-goal yes
|
restricts the selection
to the proofs of verified goals (that does not mean that the proof is
verified). Same for the other cases
\verb
|
no
|
and
\verb
|
all
|
.
\item
Option
\verb
|
--filter-archived yes
|
restricts the selection
to the proofs that are archived
\index
{
archived
}
.
to the proofs that are archived.
Same for the other cases
\verb
|
no
|
and
\verb
|
all
|
except the default is
\verb
|
no
|
.
\end{itemize}
...
...
@@ -836,7 +839,7 @@ share the same set of option to specify the modification. The
subcommand
\texttt
{
mod
}
modify directly the proof attempt,
\texttt
{
copy
}
copy the proof attempt before doing the modification,
\texttt
{
copy-archive
}
mark the original proof attempt as
archived
\index
{
archived
}
.
archived.
The options are:
\begin{itemize}
\item
Option
\verb
|
--set-obsolete
|
marks the selected proofs as
...
...
doc/manual.tex
View file @
85a04de5
...
...
@@ -26,8 +26,12 @@
\setcounter
{
bottomnumber
}{
4
}
\setcounter
{
totalnumber
}{
8
}
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries
% \usepackage{glossary}
% \makeglossary
% \glossary{name={entry name}, description={entry description}}
% for ocamldoc generated pages
%\usepackage{ocamldoc}
...
...
@@ -220,8 +224,6 @@ are the following.
\part
{
Reference Manual
}
% \input{glossary.tex}
\input
{
install.tex
}
\input
{
manpages.tex
}
...
...
@@ -248,6 +250,9 @@ are the following.
%\input{biblio-demons}
% \cleardoublepage
% \input{glossary.tex}
\cleardoublepage
\listoffigures
\cleardoublepage
...
...
doc/starting.tex
View file @
85a04de5
...
...
@@ -164,7 +164,7 @@ attempts and transformations were saved in a database --- an XML file
created when the
\why
file was opened in the GUI for the first
time. Then, for all the goals that remain unchanged, the previous
proofs are shown again. For the parts that changed, the previous
proofs attempts are shown but marked with "(obsolete)"
\index
{
obsolete
}
proofs attempts are shown but marked with "(obsolete)"
\index
{
obsolete
!proof attempt
}
so that you
know the results are not accurate. You can now retry to prove all what
remains unproved using any of the provers.
...
...
@@ -172,7 +172,7 @@ remains unproved using any of the provers.
\subsection
{
Replaying obsolete proofs
}
Instead of pushing a prover's button to rerun its proofs, you can
\emph
{
replay
}
the existing but obsolete
\index
{
obsolete
}
\emph
{
replay
}
the existing but obsolete
proof attempts, by clicking on
the
\textsf
{
Replay
}
button. By default,
\textsf
{
Replay
}
only replays
proofs that were successful before. If you want to replay all of them,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment