Commit 28e84fe8 authored by François Bobot's avatar François Bobot
Browse files

Merge remote-tracking branch 'origin/master' into computer_division_for_master

parents 53109ace 116df251
......@@ -14,14 +14,17 @@ with contributions of
Simon Cruanes
Sylvain Dailler
Clément Fumex
Leon Gondelman
Léon Gondelman
David Hauzar
Daisuke Ishii
Johannes Kanig
Mikhail Mandrykin
David Mentré
Benjamin Monate
Kim Nguyễn
Thi-Minh-Tuyen Nguyen
Mário Pereira
Raphaël Rieu-Helft
Simão Melo de Sousa
Asma Tafat
Piotr Trojanek
......
:x: marks a potential source of incompatibility
Version 1.0.0, June 25, 2018
----------------------------
Core
* improved support of counter-examples
Language
* numerous changes to syntax, see documentation appendix :x:
* `let function`, `let predicate`, `val function`, and `val predicate`
introduce symbols in both logic and programs
* attribute `[@vc:sp]` on an expression switches from traditional WP
to Flanagan-Saxe-like VC generation
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type `int` in the standard library) :x:
Language
* numerous changes to syntax, see documentation appendix :x:
* `let function`, `let predicate`, `val function`, and `val predicate`
introduce symbols in both logic and programs
* added overloading of program symbols
* new clause `alias` in function contracts :x:
* support for multiple assignments
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* new contract clause `alias { <term> with <term>, ... }` :x:
* support for parallel assignment `<term>,... <- <term>,...`
* support for local exceptions using `exception ... in ...`
* added `break`, `continue`, and `return` statements
* support for `exception` branches in `match` constructs
* support for `for` loops on range types
(including machine integers from the standard library)
* attribute `[@vc:sp]` on an expression switches from traditional WP to
Flanagan-Saxe-like VC generation
* support for type coercions in logic using `meta coercion`
* deprecated `theory`; use `module` instead
* keyword `theory` is deprecated; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x:
* cloned axioms turn into lemmas; use `with axiom my_axiom`
or `with axiom .` to keep them as axioms :x:
* `any <type> <spec>` produces an existential precondition;
use `val f : <type> <spec> in ...` (unsafe!) instead :x:
* `use T` and `clone T` now import the generated namespace T;
use `use T as T` and `clone T as T` to prevent this :x:
* `pure { <term> }` produces a ghost value in program code
Standard library
* machine integers in `mach.int.*` are now range types :x:
......@@ -34,20 +44,21 @@ Standard library
Extraction
* improved extraction to OCaml
* added partial extraction to C using the memory model of `mach.c`
* added extraction to CakeML (using 'why3 extract -D cakeml ...')
* added extraction to CakeML (using `why3 extract -D cakeml ...`)
Transformations
* transformations can now have arguments
* added transformations `assert`, `apply`, `cut`, `rewrite`, etc, à la Coq
* added transformations `assert`, `apply`, `cut`, `rewrite`, etc., à la Coq
* added transformations for reflection-based proofs
Drivers
* support for `use` in theory drivers
IDE
* replaced left toolbar by a contextual menu
* source is now editable
* premises are no longer implicitly introduced
* command-line interface to call transformations and provers
* added textual interface to call transformations and provers
Tools
* deprecated `.why` file extension; use `.mlw` instead
......@@ -56,6 +67,9 @@ Provers
* removed the `why3` Coq tactic :x:
* dropped support for Coq 8.4 :x:
Miscellaneous
* moved the opam base package to `why3`; added `why3-ide` and `why3-coq`
Version 0.88.3, January 11, 2018
--------------------------------
......
......@@ -158,8 +158,8 @@ endif
.PHONY: install-bash install-emacs install-framac
.PHONY: uninstall-bash uninstall-emacs uninstall-framac
.PHONY: ide install-ide uninstall-ide
.PHONY: coq install-coq uninstall-coq
.PHONY: pvs install-pvs uninstall-pvs
.PHONY: coq install-coq uninstall-coq clean-coq
.PHONY: pvs install-pvs uninstall-pvs clean-pvs
.PHONY: install-isabelle
.PHONY: plugins plugins.byte plugins.opt
......@@ -700,7 +700,7 @@ gallery-simple::
.PHONY: gallery-subs
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp prover multiprecision
gallery-subs::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
......@@ -708,10 +708,10 @@ gallery-subs::
echo "exporting examples/$$d"; \
mkdir -p $(GALLERYDIR)/$$d; \
cd examples/$$d; \
WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \
WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ --debug ignore_unused_vars *.mlw -o $(GALLERYDIR)/$$d; \
cd ..; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
zip -q -r $(GALLERYDIR)/$$d/$$d.zip $$d; \
git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \
cd ..; \
done
......@@ -1031,10 +1031,10 @@ COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
coq: $(COQVO) drivers/coq-realizations.aux
coq: $(COQVO) drivers/coq-realizations.aux lib/coq/version
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) lib/coq/version
clean:: clean-coq
......@@ -1170,8 +1170,6 @@ clean::
# PVS realizations
####################
ifeq (@enable_pvs_libs@,yes)
PVSLIBS_INT_FILES = Int Abs MinMax ComputerDivision EuclideanDivision
PVSLIBS_INT = $(addprefix lib/pvs/int/, $(PVSLIBS_INT_FILES))
......@@ -1194,6 +1192,13 @@ PVSLIBS_FP = $(addprefix lib/pvs/floating_point/, $(PVSLIBS_FP_ALL_FILES))
PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
$(PVSLIBS_NUMBER) $(PVSLIBS_FP)
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
drivers/pvs-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
......@@ -1209,6 +1214,15 @@ drivers/pvs-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
pvs: lib/pvs/version
clean-pvs:
rm -f lib/pvs/version
clean:: clean-pvs
ifeq (@enable_pvs_libs@,yes)
uninstall-pvs:
rm -rf $(LIBDIR)/why3/pvs
......@@ -1228,18 +1242,7 @@ install-pvs:
install:: install-pvs
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
for f in $(PVSLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T list.$$f -o lib/pvs/list/; done
for f in $(PVSLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T number.$$f -o lib/pvs/number/; done
for f in $(PVSLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/pvs-realize.drv -T floating_point.$$f -o lib/pvs/floating_point/; done
else
drivers/pvs-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
all: pvs
endif
......@@ -1641,7 +1644,7 @@ ALTERGOCMO = \
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
README examples/ \
README.md examples/ \
trywhy3_custom.css gen_index.sh \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
......@@ -2073,7 +2076,7 @@ STDLIBFILES = $(patsubst %,stdlib/%.mlw, $(STDLIBS))
# TODO: remove the hack about int.mlw once it has become builtin
stdlibdoc: $(STDLIBFILES) bin/why3doc.@OCAMLBEST@
mkdir -p doc/stdlibdoc
sed -e "s/use import Int/use import int.Int/" stdlib/int.mlw > int.mlw
sed -e "s/use Int/use int.Int/" stdlib/int.mlw > int.mlw
rm -f doc/stdlibdoc/style.css
WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L stdlib \
-o doc/stdlibdoc --title "Why3 Standard Library" \
......
......@@ -112,7 +112,6 @@
============ Making a release ============
* check the BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
......@@ -125,6 +124,7 @@
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
- check/update the authors in doc/manual.tex
- check that macro \todo is commented out in doc/macros.tex
- do "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
......
VERSION=0.90+git
VERSION=1.0.0
......@@ -15,6 +15,7 @@ suffix=$1
goods () {
pgm="bin/why3prove$suffix"
ERROR=
test -d $1 || exit 1
rm -f bench_errors
for f in $1/*.[wm][hl][yw] ; do
printf " $f... "
......@@ -45,6 +46,7 @@ goods () {
bads () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.[wm][hl][yw] ; do
printf " $f... "
if $pgm $2 $f > /dev/null 2>&1; then
......@@ -59,6 +61,7 @@ bads () {
drivers () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
if [[ $f == drivers/c.drv ]]; then continue; fi
......@@ -76,6 +79,7 @@ drivers () {
valid_goals () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.mlw; do
printf " $f... "
if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
......@@ -90,6 +94,7 @@ valid_goals () {
invalid_goals () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.mlw; do
printf " $f... "
if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
......@@ -105,6 +110,7 @@ invalid_goals () {
replay () {
pgm="bin/why3replay$suffix"
test -d $1 || exit 1
for f in $1/*/; do
printf " $f... "
if $pgm $2 $f > /dev/null 2> /dev/null; then
......@@ -182,7 +188,7 @@ extract_and_run () {
}
extract_and_test_wmp () {
dir="examples/in_progress/multiprecision"
dir=$1
shift
printf " $dir... "
printf "clean... "
......@@ -255,6 +261,7 @@ goods bench/typing/x-good --parse-only
bads bench/typing/x-good --type-only
goods bench/programs/good
goods bench/ce
goods src/trywhy3/examples "--debug ignore_missing_diverges"
goods examples/bts
goods examples/tests
goods examples/tests-provers
......@@ -270,6 +277,7 @@ goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_201
goods examples/double_wp "-L examples/double_wp"
goods examples/ring_decision "-L examples/ring_decision"
goods examples/multiprecision "-L examples/multiprecision"
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
goods examples/in_progress
echo ""
......@@ -291,6 +299,7 @@ replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_20
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/ring_decision "-L examples/ring_decision --merging-only"
replay examples/multiprecision "-L examples/multiprecision --merging-only"
replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo ""
......@@ -346,7 +355,8 @@ extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,
echo ""
echo "=== Checking extraction to C ==="
extract_and_test_wmp
extract_and_test_wmp examples/in_progress/multiprecision
extract_and_test_wmp examples/multiprecision
echo ""
echo "=== Checking --list-* ==="
......
\begin{tabular}{| l |c |c |c |c |c |}
\hline Proof obligations & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\
\cline{2-4}
\quad\subgoal{1.}{1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-4}
\quad\subgoal{2.}{2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & \valid{0.00} & \noresult& \unknown{0.00} \\
\begin{tabular}{|l|l|l|l|c|c|}
\hline Proof obligations & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
\hline
\explanation{G1} & \valid{0.00} & \noresult\\
\hline
\explanation{G2} & \unknown{0.00} & \noresult\\
\cline{2-3}
\quad\transformation{split\_goal\_right} & \multicolumn{2}{|c|}{}\\
\cline{2-3}
\quad\subgoal{G2.0}{1} & \unknown{0.00} & \unknown{0.29} \\
\cline{2-3}
\quad\subgoal{G2.1}{2} & \valid{0.00} & \noresult\\
\hline
\explanation{G3} & \valid{0.00} & \noresult\\
\hline \end{tabular}
\begin{tabular}{| l |c |c |c |c |c |}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
& \explanation{1.} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-5}
& \explanation{2.} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & & \valid{0.00} & \noresult& \unknown{0.00} \\
\begin{tabular}{|l|l|l|l|c|c|}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
\hline
\explanation{G1} & & \valid{0.00} & \noresult\\
\hline
\explanation{G2} & & \unknown{0.00} & \noresult\\
\cline{2-3}
& \explanation{G2.0} & \unknown{0.00} & \unknown{0.29} \\
\cline{2-4}
& \explanation{G2.1} & \valid{0.00} & \noresult\\
\hline
\explanation{G3} & & \valid{0.00} & \noresult\\
\hline \end{tabular}
......@@ -189,8 +189,8 @@ constructed.
Here is the way we build the formula $2+2=4$. The main difficulty is to
access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
Chap~\ref{sec:library}).
the standard theory \texttt{Int} of the file \texttt{int.why}.
% (see Chap~\ref{sec:library}).
\lstinputlisting{generated/logic__buildfmla.ml}
An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed
......@@ -296,7 +296,7 @@ quantifier.
\lstinputlisting{generated/transform__negate.ml}
The following illustrates how to turn such an OCaml function into a
transformation in the sens of Why3 API. moreover, it registers that
transformation in the sense of the Why3 API. Moreover, it registers that
transformation to make it available for example in Why3 IDE.
\lstinputlisting{generated/transform__register.ml}
......@@ -331,7 +331,7 @@ module, then the module itself called \verb|Program|.
\lstinputlisting{generated/mlw_tree__openmodule.ml}
Notice the use of a first
simple helper function \verb|mk_ident| to build an identifier without
any label nor any location.
any attributes nor any location.
To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
......@@ -367,7 +367,7 @@ file, under the form of a map of module names to modules.
\lstinputlisting{generated/mlw_tree__closemodule.ml}
We can then construct the proofs tasks for our module, and then try to
call the Alt-Ergo prover. The reste of that code is using OCaml
call the Alt-Ergo prover. The rest of that code is using OCaml
functions that were already introduced before.
\lstinputlisting{generated/mlw_tree__checkingvcs.ml}
......
......@@ -118,8 +118,14 @@ extraction command line:
\paragraph{Examples.}
We illustrate different ways of using the \texttt{extract} command through some
examples. Consider the program in Figure~\ref{fig:AQueue} on
page~\pageref{fig:AQueue}. If we are only interested in extracting function
examples.
\begin{latexonly}
Consider the program in Figure~\ref{fig:AQueue} on page~\pageref{fig:AQueue}.
\end{latexonly}
\begin{htmlonly}
Consider the program of Section~\ref{sec:AQueue}.
\end{htmlonly}
If we are only interested in extracting function
\texttt{enqueue}, we can proceed as follows:
\begin{verbatim}
> why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml
......
doc/gui-3.png

44.1 KB | W: | H:

doc/gui-3.png

43.1 KB | W: | H:

doc/gui-3.png
doc/gui-3.png
doc/gui-3.png
doc/gui-3.png
  • 2-up
  • Swipe
  • Onion skin
doc/hello_proof.png

20.7 KB | W: | H:

doc/hello_proof.png

20.3 KB | W: | H:

doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
  • 2-up
  • Swipe
  • Onion skin
......@@ -12,7 +12,7 @@ package manager. It is as simple as
\begin{verbatim}
> opam install why3
\end{verbatim}
Then jump to Sec.~\ref{provers} to install external provers.
Then jump to Section~\ref{provers} to install external provers.
\subsection{Installation Instructions from Source Distribution}
......@@ -85,7 +85,7 @@ make install
\end{verbatim}
Installation can be tested as follows:
\begin{enumerate}
\item install some external provers (see~Sec.~\ref{provers} below)
\item install some external provers (see Section~\ref{provers} below)
\item run \verb|why3 config --detect|
\item run some examples from the distribution, \eg you should
obtain the following (provided the required provers are installed on
......@@ -137,7 +137,7 @@ have to run the following command:
> why3 config --detect
\end{verbatim}
It scans your \texttt{PATH} for provers and updates your configuration
file (see Sec.~\ref{sec:why3config}) accordingly.
file (see Section~\ref{sec:why3config}) accordingly.
\subsection{Multiple Versions of the Same Prover}
......
......@@ -315,18 +315,27 @@ transformations have changed (new version of \why), \why will detect
that. Since the provers might answer differently on these new
proof obligations, the corresponding proof attempts are marked obsolete.
\subsection{Context Menu}
\subsection{Menus}
The left toolbar that was present in former versions of Why3 is now
replaced by a context menu activited by clicking the right mouse button,
while cursor is on a given row of the proof session tree.
\begin{description}
\item[Context menu]\emptyitem This menu is selected by the mouse right button on some row of the task tree view.
\begin{description}
\item[provers] The detected provers are listed. Note that you can hide some provers of that list using the preferences, tab \textsf{Provers}.
\item[strategies] the set of known strategies is listed
\item[Edit] starts an editor on the selected task.
\item[Replay valid obsolete proofs] all proof nodes below the selected nodes that are obsolete but whose former status was Valid are replayed.
\item[Replay all obsolete proofs] all proof nodes below the selected nodes that are obsolete are replayed.
\item[Remove] removes a proof attempt or a transformation.
\item[Clean] removes any unsuccessful proof attempt for which there is
another successful proof attempt for the same goal
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
\end{description}
\subsection{Global Menus}
\begin{description}
\item[Menu \textsf{File}]\emptyitem
\begin{description}
\item[Add File to session] adds a file in the current proof session.
......@@ -392,8 +401,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\item[Mark obsolete] marks all the proof as
obsolete. This allows to replay every proof.
\item[Interrupt] cancels all the proof attempts currently scheduled
but not yet started.
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
\item[Bisect] performs a reduction of the context for the the current selected proof attempt, which must be a Valid one.
......@@ -445,6 +453,29 @@ available as a textual command. However the textual interface allows
for much more possibilities, including the ability to invoke
transformations with arguments.
\subsection{Key shortcuts}
\begin{itemize}
\item Save session and files : ctrl+s
\item Save all and refresh session: ctrl+r
\item Quit : ctrl+q
\item Enlarge font : ctrl+plus
\item Reduce font : ctrl+minus
\item Collapse proven goals : !
\item Collapse current node : -
\item Expand current node : +
\item Copy : ctrl+c
\item Paste : ctrl+v
\item Select parent node : ctrl+up
\item Select next unproven goal : ctrl+down
\item Change focus to command line : return
\item Edit : e
\item Replay : r
\item Clean : c
\item Remove : del
\item Mark obsolete : o
\end{itemize}
\subsection{Preferences Dialog}
......@@ -688,8 +719,9 @@ about the session, depending on the following specific options.
the session as edited proofs.
\item[\texttt{-{}-stats}] prints various proofs statistics, as
detailed below.
\item[\texttt{-{}-tree}] prints the structure of the session as a
tree in ASCII, as detailed below.
% OBSOLETE
% \item[\texttt{-{}-tree}] prints the structure of the session as a
% tree in ASCII, as detailed below.
\item[\texttt{-{}-print0}] separates the results of the options
\verb|provers| and \verb|--edited-files| by the character number 0
instead of end of line \verb|\n|. That allows you to safely use
......@@ -708,36 +740,39 @@ why3 session info --edited-files --print0 vstte12_bfs.mlw | \
\end{description}
\paragraph{Session Tree}
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.
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|.
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\scriptsize
\begin{verbatim}
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)
|-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
| | | `-Alt-Ergo (0.94)
| | `-G2.1?-+-Coq (8.3pl4)?
| | |-Simplify (1.5.4)?
| | `-Alt-Ergo (0.94)?
| |-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)?
`-G1---Simplify (1.5.4)
\end{verbatim}
}
% OBSOLETE
% \paragraph{Session Tree}
% 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.
% 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|.