Email Gateway (Aug 19 2022 at 11:18): Email Gateway (Aug 19 2022 at 11:18):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Dear all,
Is there a simple way to suppress all proofs when presenting theories
with Isabelle/Latex?
Thanks a lot,
Stephan
Email Gateway (Aug 19 2022 at 11:18):From: Holger Blasum <hbl@sysgo.com>
Dear Stephan,
On 06-21, Stephan van Staden wrote:
Is there a simple way to suppress all proofs when presenting
theories with Isabelle/Latex?
Yes. Use option document_variants="document:outline=/proof".
FWIW (there may be better ways), inlined an excerpt from my working
cheatsheet:
\subsection{PDF generation}
\paragraph{Proper PDF generation nowadays}
The new way is to have file called ``ROOT'':
\begin{lstlisting}
session "test" = "HOL" +
options [document = pdf, document_output = "output", document_variants="document:outline=/proof", quick_and_dirty=true]
theories [document = false]
(* Foo Bar *)
theories
test
files "document/root.tex"
\end{lstlisting}
Then invoke:
\begin{lstlisting}
$ isabelle build -D .
\end{lstlisting}
Explanation:
\begin{itemize}
\item document\_output'' forces generation of output into directory output (must exist)
\item outline=/proof'' forces generation of an {\em additional} file called outline.pdf'' which is not containing proofs, documented in Isabelle documentation system.pdf, Section Isabelle Sessions and Build Management'', System build options'' (in particular see p. 21 in Isabelle 2013 version of system.pdf)
\item quick\_and\_dirty=true'': allows sorry
\item ``document/root.tex'' see below (old way)
\end{itemize}
\paragraph{Printing with usedir, old way}
The old way is:
\begin{lstlisting}
$ isabelle usedir -d pdf HOL .
\end{lstlisting}
needs document/root.tex with
\begin{lstlisting}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{}
\author{}
\maketitle
\tableofcontents
\parindent 0pt\parskip 0.5ex
\input{session}
\end{document}
\end{lstlisting}
and ROOT.ML with
\begin{lstlisting}
quick_and_dirty := true;
use_thy "test";
\end{lstlisting}
Note that this automatically adds included theories to the document.
If quick\_and\_dirty is omitted only theories without cheating (``sorry'')
are accepted.
\paragraph{Quick scratch notes}
From Proof General, do ``Isabelle $\rightarrow$ Commands $\rightarrow$ display draft''.
From Isabelle/jedit use the Isar command display\_drafts ``file-name''. From Isabelle/Eclipse, I have not figured out how to use display\_drafts, but print\_drafts (sending to default printer) can be used.
display\_drafts and print\_drafts is documented in isar-ref.pdf, Document preparation'', Draft presentation''.
\paragraph{Printable comments}
Printable comments can be specified as follows:
\begin{lstlisting}
text {* *}
--"this is a comment"
\end{lstlisting}
The second version can be used within proof steps.
Within \{* text *\} blocks, underscores need to be escaped once.
When ``--'' is used, underscores need to be escaped twice.
best,
Email Gateway (Aug 19 2022 at 11:19):From: Makarius <makarius@sketis.net>
On Sat, 22 Jun 2013, Holger Blasum wrote:
\paragraph{Printing with usedir, old way}
The old way is:
\begin{lstlisting}
$ isabelle usedir -d pdf HOL .
\end{lstlisting}
BTW, Isabelle2013 is the last version where the ancient "isabelle usedir"
is still there as historical leftover. So starting from the next release,
everybody will save a lot of time, by using regular "isabelle build"
instead.
At some point I also hope to see document preparation as part of the
Prover IDE. Only nostalgy associates latex documents with some batch
build job, there are no particular technical reasons (apart from
historical legacy getting in the way as usual).
display\_drafts and print\_drafts is documented in isar-ref.pdf,
Document preparation'',Draft presentation''.
In Isabelle/jEdit you can also use the regular "File / Print" operation on
text buffers. The output quality is surprisingly high with the default
IsabelleText font.
Makarius
Email Gateway (Aug 19 2022 at 11:19):From: Joachim Breitner <breitner@kit.edu>
Hi,
does this mean that in the future it will not be possible to have a
script or makefile that will, say, create Isabelle course task and
solutions PDFs from Isabelle sources automatically and without firing up
a GUI program? Or are you merely stating that batch builds should not be
the _only_ way to create documents from Isabelle sources?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 11:19):From: Makarius <makarius@sketis.net>
The two things that are "current" in Isabelle2013 are the batch build and
the Prover IDE document interaction model. I am trying to converge both
to use more and more the same technology (for some years already). So
batch mode is definitely not going to disappear, just odd historic things
that used to be batch-mode only in the past.
Anything apart from proper "build" and "document editing" is more or less
legacy. Better forget that "isabelle usedir" with ROOT.ML or "isabelle
make" with IsaMakefile ever existed.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC