Create latex outline

Signed-off-by: Sky Wilshaw <[email protected]>

ConNF.lean

@@ -18,7 +18,6 @@ import ConNF.Construction.Code
 import ConNF.Construction.NewModelData
 import ConNF.Counting.BaseCoding
 import ConNF.Counting.BaseCounting
-import ConNF.Counting.CodingFunction
 import ConNF.Counting.Conclusions
 import ConNF.Counting.CountSupportOrbit
 import ConNF.Counting.Recode
@@ -55,6 +54,7 @@ import ConNF.ModelData.Support
 import ConNF.Position.BasePositions
 import ConNF.Position.Deny
 import ConNF.Position.Position
+import ConNF.Strong.CodingFunction
 import ConNF.Strong.SMulSpec
 import ConNF.Strong.Spec
 import ConNF.Strong.SpecSame

ConNF/Counting/Recode.lean

@@ -1,5 +1,5 @@
 import ConNF.Counting.Twist
-import ConNF.Counting.CodingFunction
+import ConNF.Strong.CodingFunction
 
 /-!
 # Recoding

ConNF/Strong/Spec.lean

@@ -1,5 +1,5 @@
 import ConNF.FOA.Inflexible
-import ConNF.Counting.CodingFunction
+import ConNF.Strong.CodingFunction
 
 /-!
 # Specifications for supports

Old/ConNF/Counting.lean

@@ -1,4 +1,4 @@
-import ConNF.Counting.CodingFunction
+import ConNF.Strong.CodingFunction
 import ConNF.Counting.Spec
 import ConNF.Counting.SpecSMul
 import ConNF.Counting.SpecSame

Old/ConNF/Counting/Recode.lean

@@ -1,5 +1,5 @@
 import ConNF.Counting.Hypotheses
-import ConNF.Counting.CodingFunction
+import ConNF.Strong.CodingFunction
 import ConNF.Counting.SupportOrbit
 import ConNF.Counting.Twist
 

Old/ConNF/Counting/Spec.lean

@@ -1,6 +1,6 @@
 import ConNF.Mathlib.Support
 import ConNF.FOA.Basic.Flexible
-import ConNF.Counting.CodingFunction
+import ConNF.Strong.CodingFunction
 import ConNF.Counting.StrongSupport
 
 /-!

latex/main.tex

@@ -1,6 +1,7 @@
-\documentclass{report}
+\documentclass{book}
 
 \usepackage[a4paper]{geometry}
+\usepackage{minitoc}
 
 \usepackage{fontspec}
 \usepackage{unicode-math}
@@ -9,7 +10,7 @@
 	BoldFont=*-Bold.otf,
 	ItalicFont=*-Italic.otf,
 	BoldItalicFont=*-BoldItalic.otf,
-	]{STIXTwoText}
+	]{STIXTwoText}[Numbers={OldStyle,Monospaced}, Ligatures=TeX]
 \setsansfont[Path=../fonts/Source_Sans_3/static/]{SourceSans3-Regular.ttf}[Ligatures={Common,TeX}]
 \setmathfont[Path=../fonts/STIXTwo/]{STIXTwoMath-Regular.otf}
 \setmathfont[Path=../fonts/,range=\star]{TeXGyrePagellaMath.otf}
@@ -19,6 +20,16 @@
   ItalicFont=*-RegularItalic.ttf,
   BoldItalicFont=*-BoldItalic.ttf]{JuliaMono}
 
+\usepackage{xcolor}
+\usepackage{hyperref}
+\usepackage{cleveref}
+\hypersetup{
+	colorlinks=true,
+	linkcolor=red!50!black,
+	citecolor=green!50!black,
+	urlcolor=magenta!70!black,
+}
+
 \usepackage[outputdir=build]{minted}
 \newmintinline[lean]{'lean4.py:Lean4Lexer -x'}{fontsize=\footnotesize,bgcolor=white}
 \newminted[leancode]{'lean4.py:Lean4Lexer -x'}{fontsize=\scriptsize,breaklines}
@@ -27,12 +38,41 @@
 
 \begin{document}
 
-\renewcommand\thechapter{\Roman{chapter}}
+% Replaces "chapter 2" with "chapter II" and "section 2.4" with "section 4"
+% \renewcommand{\thechapter}{\Roman{chapter}}
+% \renewcommand{\thesection}{\arabic{section}}
+
+\begin{titlepage}
+	\begin{center}
+		\vspace*{1cm}
+
+		\Huge
+		\textbf{\emph{New Foundations} is consistent: documentation of the formal proof}
+
+		\vspace{0.5cm}
+		\LARGE
+		Sky Wilshaw
+
+		\vfill
 
+		\Large
+		University of Nottingham\\
+		2022--\the\year{}
+
+	\end{center}
+\end{titlepage}
+
+\dominitoc{}
+
+\setcounter{tocdepth}{1}
 \tableofcontents
+\newpage
+\setcounter{tocdepth}{3}
 
 \chapter{The base type}
 
+\minitoc
+
 \input{generated/Base/Params.tex}
 \input{generated/Base/Small.tex}
 \input{generated/Base/TypeIndex.tex}
@@ -41,4 +81,91 @@ \chapter{The base type}
 \input{generated/Base/NearLitter.tex}
 \input{generated/Base/BasePerm.tex}
 
+\chapter{Ambient higher type structure}
+
+\minitoc
+
+\input{generated/Levels/Path.tex}
+\input{generated/Levels/Tree.tex}
+\input{generated/Levels/StrPerm.tex}
+\input{generated/Levels/StrSet.tex}
+
+\chapter{Position functions}
+
+\minitoc
+
+\input{generated/Position/Position.tex}
+\input{generated/Position/Deny.tex}
+\input{generated/Position/BasePositions.tex}
+
+\chapter{Model data}
+
+\minitoc
+
+\input{generated/ModelData/Enumeration.tex}
+\input{generated/ModelData/PathEnumeration.tex}
+\input{generated/ModelData/Support.tex}
+\input{generated/ModelData/ModelData.tex}
+\input{generated/ModelData/Fuzz.tex}
+\input{generated/ModelData/Level.tex}
+\input{generated/ModelData/CoherentData.tex}
+
+\chapter{The model construction}
+
+\minitoc
+
+\input{generated/Construction/Code.tex}
+\input{generated/Construction/NewModelData.tex}
+
+\chapter{Freedom of action}
+
+\minitoc
+
+\input{generated/FOA/Inflexible.tex}
+\input{generated/FOA/Coherent.tex}
+\input{generated/FOA/BaseApprox.tex}
+\input{generated/FOA/StrApprox.tex}
+\input{generated/FOA/StrApproxFOA.tex}
+\input{generated/FOA/BaseAction.tex}
+\input{generated/Background/PermutativeExtension.tex}
+\input{generated/FOA/FlexApprox.tex}
+\input{generated/FOA/StrAction.tex}
+\input{generated/FOA/StrActionFOA.tex}
+
+\chapter{Strong supports}
+
+\minitoc
+
+\input{generated/Strong/Strong.tex}
+\input{generated/Strong/CodingFunction.tex}
+\input{generated/Strong/Spec.tex}
+\input{generated/Strong/SMulSpec.tex}
+\input{generated/Strong/SpecSame.tex}
+
+\chapter{The counting argument}
+
+\minitoc
+
+\input{generated/Counting/Twist.tex}
+\input{generated/Counting/Recode.tex}
+\input{generated/Counting/CountSupportOrbit.tex}
+\input{generated/Counting/BaseCoding.tex}
+\input{generated/Counting/BaseCounting.tex}
+\input{generated/Counting/Conclusions.tex}
+
+\chapter{Building the model}
+
+\minitoc
+
+\input{generated/Model/InductionStatement.tex}
+\input{generated/Model/ConstructMotive.tex}
+\input{generated/Model/ConstructHypothesis.tex}
+\input{generated/Background/InductiveConstruction.tex}
+\input{generated/Model/RunInduction.tex}
+\input{generated/Model/Externalise.tex}
+\input{generated/Model/RaiseStrong.tex}
+\input{generated/Model/TTT.tex}
+\input{generated/Model/Hailperin.tex}
+\input{generated/Model/Result.tex}
+
 \end{document}

latex/weave.py

@@ -76,8 +76,6 @@ def lean_to_latex(lean: str):
 
 # Converts a block of markdown documentation to latex.
 def docs_to_latex(docs: str):
-    # Convert inline code.
-    docs = re.sub(r'`(.*?)`', r'\\lean{\1}', docs)
     # Convert italics.
     docs = re.sub(r'\*([^ ].*?)\*', r'\\textit{\1}', docs)
     # Convert quote marks.
@@ -86,9 +84,27 @@ def docs_to_latex(docs: str):
 
     output = ''
     in_list = False
+    in_code_block = False
     for line in docs.splitlines():
+        if in_code_block:
+            if line.startswith('```'):
+                # End this code block.
+                in_code_block = False
+                output += '\n' + r'\begin{leancode}' + '\n' + current_code_block.strip() + '\n' + r'\end{leancode}'
+            else:
+                current_code_block += line + '\n'
+            continue
+        if line.startswith('```'):
+            # Start a code block.
+            in_code_block = True
+            current_code_block = ""
+            continue
+
         output += '\n'
 
+        # Convert inline code.
+        line = re.sub(r'`(.*?)`', r'\\lean{\1}', line)
+
         if line.startswith('* '):
             if not in_list:
                 output += r'\begin{itemize}' + '\n'