diff --git a/latex/justfile b/latex/justfile index 8d135d9c9f..896d1c7eae 100644 --- a/latex/justfile +++ b/latex/justfile @@ -1,2 +1,7 @@ +all: weave tex + tex: latexmk -shell-escape -pdf -pdflatex=lualatex -file-line-error -halt-on-error -interaction=nonstopmode -cd -output-directory=build ./main.tex + +weave: + python3 weave.py diff --git a/latex/lean4.py b/latex/lean4.py index b44d2a0423..a20043d547 100644 --- a/latex/lean4.py +++ b/latex/lean4.py @@ -136,7 +136,7 @@ class Lean4Lexer(RegexLexer): """ For the Lean 4 theorem prover. """ - + name = 'Lean4' url = 'https://github.com/leanprover/lean4' aliases = ['lean4'] @@ -208,6 +208,7 @@ class Lean4Lexer(RegexLexer): (r'\S', Name.Builtin.Pseudo), ], 'root': [ + (r'<[0-9]+ lines?>', Keyword.Constant), (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), (r'@\[', Keyword.Declaration, 'attribute'), diff --git a/latex/main.tex b/latex/main.tex index ace009e6a4..88c9c2c015 100644 --- a/latex/main.tex +++ b/latex/main.tex @@ -1,4 +1,6 @@ -\documentclass{article} +\documentclass{report} + +\usepackage[a4paper]{geometry} \usepackage{fontspec} \usepackage{unicode-math} @@ -19,14 +21,24 @@ \usepackage[outputdir=build]{minted} \newmintinline[lean]{'lean4.py:Lean4Lexer -x'}{fontsize=\footnotesize,bgcolor=white} -\newminted[leancode]{'lean4.py:Lean4Lexer -x'}{fontsize=\footnotesize} +\newminted[leancode]{'lean4.py:Lean4Lexer -x'}{fontsize=\scriptsize,breaklines} \usemintedstyle{xcode} \begin{document} -An example of Lean code. \lean{foo bar}. +\renewcommand\thechapter{\Roman{chapter}} + +\tableofcontents + +\chapter{The base type} -\input{generated/Construction/Code.latex} +\input{generated/Base/Params.tex} +\input{generated/Base/Small.tex} +\input{generated/Base/TypeIndex.tex} +\input{generated/Base/Litter.tex} +\input{generated/Base/Atom.tex} +\input{generated/Base/NearLitter.tex} +\input{generated/Base/BasePerm.tex} \end{document} diff --git a/latex/weave.py b/latex/weave.py index 7612a4df7d..569831126e 100644 --- a/latex/weave.py +++ b/latex/weave.py @@ -1,17 +1,144 @@ import os +import re -# Converts lean code to latex. -def convert(lean): - return r'\begin{leancode}' + '\n' + lean + '\n' + r'\end{leancode}' +omit_proofs = True +# Converts a block of lean code to latex. +def lean_to_latex(lean: str): + # Remove imports. + lean = re.sub(r'import .*', '', lean) + # Remove `open` declarations. + lean = re.sub(r'open .*', '', lean) + # Remove `universe` declarations. + lean = re.sub(r'universe .*', '', lean) + # Remove `namespace ConNF` and `end ConNF`. + lean = lean.replace('namespace ConNF', '') + lean = lean.replace('end ConNF', '') + # Remove `noncomputable section`. + lean = lean.replace('noncomputable section', '') + + # Replace any triple newlines that we just created with double newlines. + while True: + old_lean = lean + lean = lean.replace('\n\n\n', '\n\n') + if old_lean == lean: + break + + if omit_proofs: + # Remove large tactic blocks. + # If `by` occurs at the end of a line with some indent level, then depending on the next line's + # indent level, we do different things. + # If the next line is at a lower indent level, the proof is considered to run until we get + # back to indent level 0. + # If the next line is at a higher indent level, the proof is considered to end once we get + # back to the original indent level. + + output = "" + in_large_proof = False + for line in lean.splitlines(): + indent_result = re.search(r' *', line) + indent = indent_result.end() - indent_result.start() + + if in_large_proof: + if proof_target_indent is None: + if indent < by_indent: + proof_target_indent = 0 + else: + proof_target_indent = by_indent + if indent <= proof_target_indent: + # The proof is done. + in_large_proof = False + if proof_target_indent == 0: + output += "\n " + if proof_lines == 1: + output += " <1 line>" + else: + output += f" <{proof_lines} lines>" + else: + # Consume this line entirely. + proof_lines += 1 + continue + + output += '\n' + line + if line.endswith(':= by'): + in_large_proof = True + by_indent = indent + proof_target_indent = None + proof_lines = 0 + else: + output = lean + + output = output.strip() + if output == '': + return '' + else: + return r'\begin{leancode}' + '\n' + output + '\n' + r'\end{leancode}' + '\n' + +# 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. + docs = re.sub(r'"([^ ].*?)"', '``\\1\'\'', docs) + docs = re.sub(r'\'([^ ].*?)\'', '`\\1\'', docs) + + output = '' + in_list = False + for line in docs.splitlines(): + output += '\n' + + if line.startswith('* '): + if not in_list: + output += r'\begin{itemize}' + '\n' + in_list = True + output += r'\item ' + line[2:] + continue + elif not line.startswith(' '): + if in_list: + output += r'\end{itemize}' + '\n' + in_list = False + + done = False + for i in range(1,6): + if line.startswith('#' * i + ' '): + output += '\\' + ('sub' * (i - 1)) + 'section{' + line[i + 1:] + '}' + done = True + break + if done: continue + + output += line + + if in_list: + output += '\n' + r'\end{itemize}' + + return output.strip() + '\n' + +# Converts an entire file of lean code to latex. +def convert(lean: str): + # First, extract the module documentation and regular documentation blocks. + output = '' + while True: + result = re.search(r'/-[-!]', lean) + if result is None: + output += lean_to_latex(lean) + break + else: + i = lean.find('-/') + doc_block = lean[result.end():i] + output += lean_to_latex(lean[:result.start()]) + output += docs_to_latex(doc_block) + lean = lean[i+2:] + return output + +os.chdir('..') for root, dirs, files in os.walk('ConNF'): path = root.split(os.sep) newroot = os.path.join('latex', 'generated', *path[1:]) os.makedirs(newroot, exist_ok=True) for file in files: - if file != 'Code.lean': - continue with open(os.path.join(root, file)) as f: content = f.read() - with open(os.path.join(newroot, file.removesuffix('.lean') + '.latex'), 'w') as f: + with open(os.path.join(newroot, file.removesuffix('.lean') + '.tex'), 'w') as f: f.write(convert(content))