MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 9e5aab7b authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Reduce the font size of some listings. Warn when compiling documentation.

parent 1ef5d144
......@@ -1121,18 +1121,18 @@ doc/bnf: doc/bnf.mll
$(OCAMLOPT) -o $@ doc/bnf.ml
DOC = api glossary ide intro library macros manpages coq_tactic \
realizations manual starting syntax syntaxref version whyml
realizations manual starting syntax syntaxref technical version whyml
DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
cd doc; $(RUBBER) -d manual.tex
cd doc; $(RUBBER) --warn all --pdf manual.tex
# doc/manual.html: doc/manual.tex doc/version.tex
# $(MAKE) -C doc manual.html
clean::
cd doc; $(RUBBER) -d --clean manual.tex
cd doc; $(RUBBER) --pdf --clean manual.tex
else
......
......@@ -577,6 +577,7 @@ nothing. On the other hand if the proof is obsolete we mark it with an
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\footnotesize
\begin{verbatim}
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Alt-Ergo (0.93)
| `-Simplify (1.5.4)?
......@@ -589,6 +590,7 @@ hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Alt-Ergo (0.93)
| `-Simplify (1.5.4)?
`-G1---Simplify (1.5.4)
\end{verbatim}
}
\paragraph{Session Statistics}
......@@ -612,6 +614,7 @@ The proof statistics given by option \verb|--stats| are as follows:
For example, here are the session statistics produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\footnotesize
\begin{verbatim}
== Number of goals ==
total: 5 proved: 3
......@@ -633,6 +636,7 @@ proof'' example of Section~\ref{chap:starting}.
Alt-Ergo (0.93) : 2 0.02 0.02 0.02
Simplify (1.5.4) : 2 0.01 0.01 0.01
\end{verbatim}
}
\subsection{Command \texttt{latex}}
......
......@@ -18,13 +18,14 @@ installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
file is reproduced below.
\verbatiminput{../share/provers-detection-data.conf}
{\footnotesize\verbatiminput{../share/provers-detection-data.conf}}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}
\begin{figure}[p]
{\footnotesize
\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
......@@ -70,6 +71,7 @@ interactive = false
name = "Alt-Ergo"
version = "0.93"
\end{verbatim}
}
\caption{Sample why3.conf file}
\label{fig:why3conf}
\end{figure}
......
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