Commit dcb7071d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Generate some documentation images using the batch mode.

parent 7e515963
......@@ -16,3 +16,4 @@
why3session.xml merge=ours
why3shapes.gz merge=ours
*.png diff=image
......@@ -1815,6 +1815,12 @@ DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib share/provers-detection-data.conf
cd doc; $(RUBBER) --warn all --pdf manual.tex
update-doc-png:
export UBUNTU_MENUPROXY=0; \
export WHY3CONFIG=doc/why3ide-doc.conf; \
export WHY3LOADPATH=stdlib; \
sed -n -e 's/^%EXECUTE \(.*\)/\1/p' $(DOCTEX) | $(SHELL) -e
CLEANDIRS += doc
GENERATED += doc/bnf.ml
......
......@@ -25,6 +25,7 @@ we show how this file is handled in the \why GUI
(Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
executable (Section~\ref{sec:batch}).
%EXECUTE cp examples/logic/hello_proof.why doc/
\section{Getting Started with the GUI}
\label{sec:gui}
......@@ -34,9 +35,10 @@ 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.
%EXECUTE bin/why3 ide --batch "wait 1;snap doc/gui-1.png" doc/hello_proof.why
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-1.png}
\includegraphics[width=\textwidth]{gui-1.png}
\caption{The GUI when started the very first time}
\label{fig:gui1}
\end{figure}
......@@ -70,10 +72,10 @@ allows to browse inside the theories.
In this tree view, we have a structured view of the file: this file
contains one theory, itself containing three goals.
%EXECUTE bin/why3 ide --batch "type next;wait 1;snap doc/gui-2.png" doc/hello_proof.why
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-2.png}
\includegraphics[width=\textwidth]{gui-2.png}
\caption{The GUI with goal G1 selected}
\label{fig:gui2}
\end{figure}
......@@ -94,10 +96,11 @@ or the parent file. Let us now select the theory ``HelloProof'' and
click on the \textsf{Simplify} button. After a short time, you should
get the display of Figure~\ref{fig:gui3}.
%EXECUTE bin/why3 ide --batch "type alt-ergo;view source;wait 5;snap doc/gui-3.png" doc/hello_proof.why
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-3.png}
\caption{The GUI after Simplify prover is run on each goal}
\includegraphics[width=\textwidth]{gui-3.png}
\caption{The GUI after running the Alt-Ergo prover on each goal}
\label{fig:gui3}
\end{figure}
......@@ -120,10 +123,11 @@ have two subgoals, and you can try again a prover on them, for example
Simplify. We already have a lot of goals and proof attempts, so it is a good idea to close the sub-trees which are already proved: this can be done by the menu \textsf{View/Collapse proved goals}, or even better by its shortcut ``Ctrl-C''.
You should see now what is displayed on Figure~\ref{fig:gui4}.
%EXECUTE bin/why3 ide --batch "type alt-ergo;wait 5;type next;wait 1;type split_goal_wp;wait 2;snap doc/gui-4.png" doc/hello_proof.why
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-4.png}
\caption{The GUI after splitting goal $G_2$ and collapsing proved goals}
\includegraphics[width=\textwidth]{gui-4.png}
\caption{The GUI after splitting goal $G_2$}
\label{fig:gui4}
\end{figure}
......@@ -301,6 +305,8 @@ hello_proof.why HelloProof G2 : Valid (0.00s)
Section~\ref{sec:transformations} gives the description of the various
transformations available.
%EXECUTE rm doc/hello_proof.why
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
......
[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
name = "CoqIDE"
[ide]
allow_source_editing = true
current_tab = 0
default_editor = "editor %f"
default_prover = ""
error_color = "orange"
font_size = 11
goal_color = "gold"
iconset = "fatcow"
intro_premises = true
max_boxes = 16
neg_premise_color = "pink"
premise_color = "chartreuse"
print_coercions = true
print_labels = false
print_locs = false
print_time_limit = false
saving_policy = 2
show_full_context = false
task_height = 480
tree_width = 384
verbose = 0
window_height = 768
window_width = 1024
[main]
cntexample = false
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5
[prover]
command = "coqtop -batch -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
driver = "coq"
editor = "coqide"
in_place = false
interactive = true
name = "Coq"
shortcut = "coq"
version = "8.7.1"
[prover]
command = "alt-ergo -timelimit %t %f"
command_steps = "alt-ergo -steps-bound %S %f"
driver = "alt_ergo"
in_place = false
interactive = false
name = "Alt-Ergo"
shortcut = "alt-ergo"
version = "2.0.0"
......@@ -387,16 +387,16 @@ let () =
Debug.dprintf debug " done.@.";
Gconfig.init ()
let window_width,window_height,window_title =
let window_title =
match !opt_batch with
| Some _ -> 1024, 768, "Why3 Batch Mode"
| None -> gconfig.window_width, gconfig.window_height, "Why3 Interactive Proof Session"
| Some _ -> "Why3 Batch Mode"
| None -> "Why3 Interactive Proof Session"
let main_window : GWindow.window =
let w = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:window_width
~height:window_height
~width:gconfig.window_width
~height:gconfig.window_height
~title:window_title ()
in
(* callback to record the new size of the main window when changed, so
......@@ -2354,11 +2354,13 @@ let batch s =
if w > 0 then cmd := Printf.sprintf "wait %d" (w - 1) :: !cmd
| "type" :: cmd ->
let cmd = Strings.join " " cmd in
command_entry#misc#grab_focus ();
add_command list_commands cmd;
interp cmd
| ["snap"; f] ->
let s = Printf.sprintf "import -window \"%s\" %s" window_title f in
if Sys.command s <> 0 then Printf.eprintf "Command failed: %s\n%!" s
| "snap" :: cmd ->
let cmd = Strings.join " " cmd in
let cmd = Printf.sprintf "import -window \"%s\" -define png:include-chunk=none %s" window_title cmd in
if Sys.command cmd <> 0 then Printf.eprintf "Batch command failed: %s\n%!" cmd
| _ -> Printf.eprintf "Unrecognized batch command: %s\n%!" c
end;
true
......
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