Skip to content

Commit a4fab6b

Browse files
mn200mn200
committed
Start of tutorial/example on using the latex-munger
1 parent e2da77f commit a4fab6b

File tree

8 files changed

+218
-0
lines changed

8 files changed

+218
-0
lines changed

‎examples/latex-generation/paper/.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
paper.tex
2+
paper.pdf
3+
paper.fls
4+
munge
5+
holtexbasic.sty

‎examples/latex-generation/paper/Holmakefile‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
INCLUDES = ../theories
2+
3+
paper.pdf: paper.tex holtexbasic.sty
4+
latexmk -pdf paper
5+
6+
munge: ppLib.uo
7+
$(HOLDIR)/bin/mkmunge.exe -o $@ $<
8+
9+
paper.tex: paper.htex overrides munge
10+
./munge overrides < $< > $@
11+
12+
13+
holtexbasic.sty: $(HOLDIR)/src/TeX/holtexbasic.sty
14+
$(CP) $< $@
15+
16+
EXTRA_CLEANS = holtexbasic.sty paper.pdf paper.tex paper.fls paper.aux paper.fdb_latexmk paper.log munge

‎examples/latex-generation/paper/macros.tex‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
\newcommand{\bs}{\texttt{\char'134}} % backslash
2+
\newcommand{\lb}{\texttt{\char'173}} % left brace
3+
\newcommand{\rb}{\texttt{\char'175}} % right brace
4+
\newcommand{\td}{\texttt{\char'176}} % tilde
5+
\newcommand{\lt}{\texttt{\char'74}} % less than
6+
\newcommand{\gt}{\texttt{\char'76}} % greater than
7+
\newcommand{\dol}{\texttt{\char'44}} % dollar
8+
\newcommand{\pipe}{\texttt{\char'174}}
9+
\newcommand{\apost}{\texttt{\textquotesingle}}
10+
% back quote (tt font)
11+
\newcommand{\bq}{\texttt{\char'140}}
12+
% double back quotes ``
13+
\newcommand{\dq}{\bq\bq}
14+
% "fancy" versions of the same
15+
\newcommand{\fldq}{\mbox{\textrm{\textquotedblleft}}}
16+
\newcommand{\frdq}{\mbox{\textrm{\textquotedblright}}}

‎examples/latex-generation/paper/overrides‎

Whitespace-only changes.

‎examples/latex-generation/paper/paper.htex‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
\documentclass{article}
2+
3+
\usepackage{holtexbasic}
4+
\usepackage{proof}
5+
\usepackage{alltt}
6+
\include{macros.tex}
7+
8+
\renewcommand{\HOLConst}[1]{\textsf{#1}}
9+
10+
\title{Writing \LaTeX{} with Embedded HOL}
11+
\author{HOL Developers}
12+
\date{}
13+
14+
\begin{document}
15+
16+
\maketitle
17+
\begin{abstract}
18+
This document attempts to provide a tutorial-like introduction to the process of generating \LaTeX{} files (and ultimately, PDFs) that include pretty-printed material from HOL theories.
19+
While the \textsc{Description} manual includes a fairly careful description of HOL's solution to this problem (the ``munger''), it can be hard to get started using just that documentation.
20+
This document provides a simple, sample document that covers a number of standard features, and does so in a style that we hope is easy to understand.
21+
\end{abstract}
22+
23+
\section{Introduction}
24+
25+
The premise is that this document will simultaneously explain \LaTeX-munging while illustrating the use of the technology with respect to a miniature HOL formalisation (on binary trees).
26+
Under \texttt{HOL/examples/latex-generation}, we find a somewhat plausible picture:
27+
in the directory \texttt{theories}, there is a HOL development consisting of two theory files: \texttt{sampleTreeScript.sml} and \texttt{bstScript.sml}, with the latter building on the former.
28+
This represents the HOL development that is to be documented for publication in this paper.
29+
In the second directory, \texttt{paper} are all the sources for this PDF.
30+
31+
There is no requirement for the two directories to be siblings of each other in this way, but it is convenient in this context.
32+
In practice, the theory files will be in one repository (possibly quite public), and the paper will be in a separate space, possibly backed by a more private repository.
33+
34+
The basic flow is that as authors we will write a special \texttt{paper.htex} file, pretending that we are writing normal \LaTeX{} document, but with access to special extra commands (\texttt{\bs{}HOLthm\lb\dots\rb} and others) for inserting HOL material.
35+
Our source \texttt{paper.htex} file will be built into the PDF by first being translated into genuine \LaTeX{} file \texttt{paper.tex}, which can then be turned into a PDF with the usual technology (here we will assume use of \texttt{latexmk}).
36+
37+
\subsection{Manifest}
38+
39+
The following summarises the contents of the \texttt{papers} directory, with more details to come later in this document:
40+
\begin{description}
41+
\item[\texttt{.gitignore}] Specification of names of generated files that \texttt{git} should ignore so that generated files don't end up being committed to repositories.
42+
\item[\texttt{Holmakefile}] This file specifies the standard build instructions, and includes a pointer to the directory where the HOL sources are to be found in the \texttt{INCLUDES =} line.
43+
\item[\texttt{macros.tex}] A file of macros supporting our paper; this file can be (and is) perfectly standard \LaTeX, and is \texttt{\bs{}include}-d into the \texttt{paper.htex} file as one might normally proceed.
44+
\item[\texttt{overrides}] This files includes custom replacements for HOL symbols to give them prettier \LaTeX{} renderings.
45+
\item[\texttt{paper.htex}] The sources for this paper.
46+
\item[\texttt{ppLib.sml}] A small HOL ``library'' that refers to the HOL theories where the desired results are present, or which have ancestors where those results are present.
47+
In our case, the \texttt{ppLib.sml} file refers to \texttt{bstTheory}, which will give us the ability to refer to theorems from \texttt{bstTheory} and \texttt{sampleTheory} both (because the latter is an ancestor of the former, and it's impossible to have a child theory in context without also having its parent).
48+
\end{description}
49+
50+
After a call to \texttt{Holmake}, the required theories (\texttt{bst} and its ancestors) in \texttt{theories} will be rebuilt, and the following files will be generated in the \texttt{papers} directory:
51+
\begin{description}
52+
\item[\texttt{.hol}] The usual output directory containing HOL object files, logs and the like.
53+
\item[\texttt{holtexbasic.sty}] A file specifying the standard HOL \LaTeX{} macros, copied across into the working directory from the HOL source tree.
54+
\item[\texttt{munge}] The munging executable responsible for turning \texttt{paper.htex} into \texttt{paper.tex}.
55+
This program is a Unix filter, reading from \texttt{stdin} and writing to \texttt{stdout}.
56+
\item[\texttt{paper.pdf}] The PDF of this document.
57+
\item[\texttt{paper.tex}] The translated paper file, containing \LaTeX{} replacements for all of the special HOL-macros.
58+
\item[\texttt{paper.*}] A slew of the usual auxiliary files generated by \LaTeX{} and \texttt{latexmk} as the PDF is generated.
59+
\end{description}
60+
61+
\subsection{Sample Usages}
62+
63+
\noindent The output on the right is generated by writing what appears in the left column:
64+
65+
\begin{center}
66+
\begin{minipage}[t]{0.35\textwidth}
67+
\begin{alltt}
68+
Lead-in text:
69+
\bs{}begin\lb{}alltt\rb{}
70+
Alltt text:
71+
\bs{}HOLthm\lb{}bst.keys_elems\rb{}
72+
\bs{}end\lb{}alltt\rb{}
73+
The constant \bs{}HOLtm\lb{}keys\rb{}
74+
returns the set of a
75+
binary search tree's keys.
76+
\end{alltt}
77+
\end{minipage}\hfill{}
78+
\begin{minipage}[t]{0.55\textwidth}
79+
Lead-in text:
80+
\begin{alltt}
81+
Alltt text:
82+
\HOLthm{bst.keys_elems}
83+
\end{alltt}
84+
The constant \HOLtm{keys} returns the set of a binary search tree's keys.
85+
\end{minipage}
86+
\end{center}
87+
88+
\end{document}

‎examples/latex-generation/paper/ppLib.sml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
structure ppLib =
2+
struct
3+
4+
open bstTheory
5+
6+
end (* struct *)

‎examples/latex-generation/theories/bstScript.sml‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
Theory bst
2+
Ancestors sampleTree pred_set
3+
4+
Type dict = “:('a # 'b) stree”
5+
6+
Definition keys_def[simp]:
7+
keys Lf = {} /\
8+
keys (Nd t1 (k,v) t2) = {k} ∪ keys t1 ∪ keys t2
9+
End
10+
11+
Theorem keys_elems:
12+
keys d = IMAGE FST (elems d)
13+
Proof
14+
Induct_on ‘d’ >> simp[pairTheory.FORALL_PROD]
15+
QED
16+
17+
Inductive sorted_dict:
18+
[~Lf:] sorted_dict R Lf
19+
[~Nd:]
20+
sorted_dict R t1 ∧ sorted_dict R t2 ∧
21+
(∀e. e ∈ keys t1 ⇒ R e k) ∧
22+
(∀e. e ∈ keys t2 ⇒ R k e) ⇒
23+
sorted_dict R (Nd t1 (k,v) t2)
24+
End

‎examples/latex-generation/theories/sampleTreeScript.sml‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
Theory sampleTree
2+
Ancestors hol pred_set
3+
4+
5+
Datatype: stree = Lf | Nd stree 'a stree
6+
End
7+
8+
Definition inorder_def[simp]:
9+
inorder Lf = [] ∧
10+
inorder (Nd t1 a t2) = inorder t1 ++ [a] ++ inorder t2
11+
End
12+
13+
Definition elemcount_def[simp]:
14+
elemcount Lf = 0 ∧
15+
elemcount (Nd t1 _ t2) = elemcount t1 + elemcount t2 + 1
16+
End
17+
18+
Theorem elemcount_LENGTH_inorder:
19+
elemcount t = LENGTH (inorder t)
20+
Proof
21+
Induct_on ‘t’ >> simp[]
22+
QED
23+
24+
Definition flip_def[simp]:
25+
flip Lf = Lf ∧
26+
flip (Nd t1 a t2) = Nd (flip t2) a (flip t1)
27+
End
28+
29+
Definition elems_def[simp]:
30+
elems Lf = {} ∧
31+
elems (Nd t1 a t2) = {a} ∪ elems t1 ∪ elems t2
32+
End
33+
34+
Theorem elems_flip[simp]:
35+
elems (flip t) = elems t
36+
Proof
37+
Induct_on ‘t’ >> simp[AC UNION_ASSOC UNION_COMM]
38+
QED
39+
40+
Theorem elems_inorder:
41+
elems t = set (inorder t)
42+
Proof
43+
Induct_on ‘t’ >> simp[AC UNION_ASSOC UNION_COMM]
44+
QED
45+
46+
Theorem elemcount_flip[simp]:
47+
elemcount (flip t) = elemcount t
48+
Proof
49+
Induct_on ‘t’ >> simp[]
50+
QED
51+
52+
Theorem inorder_flip:
53+
inorder (flip t) = REVERSE (inorder t)
54+
Proof
55+
Induct_on ‘t’ >> simp[]
56+
QED
57+
58+
Inductive exists:
59+
[~atNd:] P a ⇒ exists P (Nd t1 a t2)
60+
[~atLeft:] exists P t1 ⇒ exists P (Nd t1 a t2)
61+
[~atRight:] exists P t2 ⇒ exists P (Nd t1 a t2)
62+
End
63+

0 commit comments

Comments
 (0)