Create blueprint template

Signed-off-by: zeramorphic <[email protected]>

blueprint/.gitignore

@@ -0,0 +1,4 @@
+print/
+web/
+web.bbl
+web.paux

blueprint/fonts/Source_Sans_3/OFL.txt

@@ -0,0 +1,93 @@
+Copyright 2010-2020 Adobe (http://www.adobe.com/), with Reserved Font Name 'Source'. All Rights Reserved. Source is a trademark of Adobe in the United States and/or other countries.
+
+This Font Software is licensed under the SIL Open Font License, Version 1.1.
+This license is copied below, and is also available with a FAQ at:
+https://openfontlicense.org
+
+
+-----------------------------------------------------------
+SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
+-----------------------------------------------------------
+
+PREAMBLE
+The goals of the Open Font License (OFL) are to stimulate worldwide
+development of collaborative font projects, to support the font creation
+efforts of academic and linguistic communities, and to provide a free and
+open framework in which fonts may be shared and improved in partnership
+with others.
+
+The OFL allows the licensed fonts to be used, studied, modified and
+redistributed freely as long as they are not sold by themselves. The
+fonts, including any derivative works, can be bundled, embedded, 
+redistributed and/or sold with any software provided that any reserved
+names are not used by derivative works. The fonts and derivatives,
+however, cannot be released under any other type of license. The
+requirement for fonts to remain under this license does not apply
+to any document created using the fonts or their derivatives.
+
+DEFINITIONS
+"Font Software" refers to the set of files released by the Copyright
+Holder(s) under this license and clearly marked as such. This may
+include source files, build scripts and documentation.
+
+"Reserved Font Name" refers to any names specified as such after the
+copyright statement(s).
+
+"Original Version" refers to the collection of Font Software components as
+distributed by the Copyright Holder(s).
+
+"Modified Version" refers to any derivative made by adding to, deleting,
+or substituting -- in part or in whole -- any of the components of the
+Original Version, by changing formats or by porting the Font Software to a
+new environment.
+
+"Author" refers to any designer, engineer, programmer, technical
+writer or other person who contributed to the Font Software.
+
+PERMISSION & CONDITIONS
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of the Font Software, to use, study, copy, merge, embed, modify,
+redistribute, and sell modified and unmodified copies of the Font
+Software, subject to the following conditions:
+
+1) Neither the Font Software nor any of its individual components,
+in Original or Modified Versions, may be sold by itself.
+
+2) Original or Modified Versions of the Font Software may be bundled,
+redistributed and/or sold with any software, provided that each copy
+contains the above copyright notice and this license. These can be
+included either as stand-alone text files, human-readable headers or
+in the appropriate machine-readable metadata fields within text or
+binary files as long as those fields can be easily viewed by the user.
+
+3) No Modified Version of the Font Software may use the Reserved Font
+Name(s) unless explicit written permission is granted by the corresponding
+Copyright Holder. This restriction only applies to the primary font name as
+presented to the users.
+
+4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
+Software shall not be used to promote, endorse or advertise any
+Modified Version, except to acknowledge the contribution(s) of the
+Copyright Holder(s) and the Author(s) or with their explicit written
+permission.
+
+5) The Font Software, modified or unmodified, in part or in whole,
+must be distributed entirely under this license, and must not be
+distributed under any other license. The requirement for fonts to
+remain under this license does not apply to any document created
+using the Font Software.
+
+TERMINATION
+This license becomes null and void if any of the above conditions are
+not met.
+
+DISCLAIMER
+THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
+OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
+COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
+DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
+OTHER DEALINGS IN THE FONT SOFTWARE.

blueprint/fonts/Source_Sans_3/README.txt

@@ -0,0 +1,79 @@
+Source Sans 3 Variable Font
+===========================
+
+This download contains Source Sans 3 as both variable fonts and static fonts.
+
+Source Sans 3 is a variable font with this axis:
+  wght
+
+This means all the styles are contained in these files:
+  Source_Sans_3/SourceSans3-VariableFont_wght.ttf
+  Source_Sans_3/SourceSans3-Italic-VariableFont_wght.ttf
+
+If your app fully supports variable fonts, you can now pick intermediate styles
+that aren’t available as static fonts. Not all apps support variable fonts, and
+in those cases you can use the static font files for Source Sans 3:
+  Source_Sans_3/static/SourceSans3-ExtraLight.ttf
+  Source_Sans_3/static/SourceSans3-Light.ttf
+  Source_Sans_3/static/SourceSans3-Regular.ttf
+  Source_Sans_3/static/SourceSans3-Medium.ttf
+  Source_Sans_3/static/SourceSans3-SemiBold.ttf
+  Source_Sans_3/static/SourceSans3-Bold.ttf
+  Source_Sans_3/static/SourceSans3-ExtraBold.ttf
+  Source_Sans_3/static/SourceSans3-Black.ttf
+  Source_Sans_3/static/SourceSans3-ExtraLightItalic.ttf
+  Source_Sans_3/static/SourceSans3-LightItalic.ttf
+  Source_Sans_3/static/SourceSans3-Italic.ttf
+  Source_Sans_3/static/SourceSans3-MediumItalic.ttf
+  Source_Sans_3/static/SourceSans3-SemiBoldItalic.ttf
+  Source_Sans_3/static/SourceSans3-BoldItalic.ttf
+  Source_Sans_3/static/SourceSans3-ExtraBoldItalic.ttf
+  Source_Sans_3/static/SourceSans3-BlackItalic.ttf
+
+Get started
+-----------
+
+1. Install the font files you want to use
+
+2. Use your app's font picker to view the font family and all the
+available styles
+
+Learn more about variable fonts
+-------------------------------
+
+  https://developers.google.com/web/fundamentals/design-and-ux/typography/variable-fonts
+  https://variablefonts.typenetwork.com
+  https://medium.com/variable-fonts
+
+In desktop apps
+
+  https://theblog.adobe.com/can-variable-fonts-illustrator-cc
+  https://helpx.adobe.com/nz/photoshop/using/fonts.html#variable_fonts
+
+Online
+
+  https://developers.google.com/fonts/docs/getting_started
+  https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_Fonts/Variable_Fonts_Guide
+  https://developer.microsoft.com/en-us/microsoft-edge/testdrive/demos/variable-fonts
+
+Installing fonts
+
+  MacOS: https://support.apple.com/en-us/HT201749
+  Linux: https://www.google.com/search?q=how+to+install+a+font+on+gnu%2Blinux
+  Windows: https://support.microsoft.com/en-us/help/314960/how-to-install-or-remove-a-font-in-windows
+
+Android Apps
+
+  https://developers.google.com/fonts/docs/android
+  https://developer.android.com/guide/topics/ui/look-and-feel/downloadable-fonts
+
+License
+-------
+Please read the full license text (OFL.txt) to understand the permissions,
+restrictions and requirements for usage, redistribution, and modification.
+
+You can use them in your products & projects – print or digital,
+commercial or otherwise.
+
+This isn't legal advice, please consider consulting a lawyer and see the full
+license for all details.

blueprint/requirements.txt

@@ -0,0 +1,8 @@
+# https://github.com/pyinvoke/invoke/issues/891
+invoke==2.2.0
+plasTeX @ git+https://github.com/plastex/plastex.git
+plastexdepgraph @ git+https://github.com/PatrickMassot/plastexdepgraph.git
+plastexshowmore @ git+https://github.com/PatrickMassot/plastexshowmore.git
+leanblueprint @ git+https://github.com/PatrickMassot/leanblueprint.git
+watchfiles==0.16.1
+pandoc==2.3

blueprint/src/chapters/abstract.tex

@@ -0,0 +1,4 @@
+\begin{abstract}
+  We give a self-contained account of a version of the proof of Holmes and Wilshaw \cite{con-nf} that Quine's set theory \emph{New Foundations} \cite{quine-nf} is consistent relative to the metatheory ZFC.
+  This version of the proof is written in a style that is particularly amenable to the formalisation in Lean \cite{leanprover-community-con-nf}; to that end, type-theoretic concerns and dependencies between parts of the proof are explicitly spelled out.
+\end{abstract}

blueprint/src/chapters/introduction.tex

@@ -0,0 +1 @@
+Foo.

blueprint/src/content.tex

@@ -0,0 +1,33 @@
+\chapter{Introduction}
+\input{chapters/introduction.tex}
+
+\chapter{Setting up the environment}
+\input{chapters/environment.tex}
+
+\chapter{Constructing the types}
+\input{chapters/construction.tex}
+
+\chapter{Freedom of action}
+\input{chapters/foa.tex}
+
+\chapter{The counting argument}
+\input{chapters/counting.tex}
+
+\chapter{Wrapping up the main induction}
+\input{chapters/induction.tex}
+
+\chapter{Verifying \texorpdfstring{\( \Con(\TTT) \)}{Con(TTT)}}
+\input{chapters/model.tex}
+
+\chapter{Model theory and verifying \texorpdfstring{\( \Con(\NF) \)}{Con(NF)}}
+\input{chapters/model_theory.tex}
+
+\chapter{Conclusion}
+\input{chapters/conclusion.tex}
+
+\appendix
+\chapter{Auxiliary results}
+\input{chapters/auxiliary.tex}
+
+\bibliographystyle{plainurl}
+\bibliography{refs}

blueprint/src/extra_styles.css

@@ -0,0 +1,53 @@
+div.theorem_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.proposition_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.lemma_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.corollary_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.proof_content {
+	border-left: .08rem solid grey;
+}
+
+figure.subfloat span.subref {
+	display: none;
+}
+
+nav.local_toc ul {
+	font-size: 1.2rem;
+}
+
+@media (min-width:1024px) {
+    nav.toc {
+        width: 25vw;
+    }
+}
+
+@media (min-width:1024px) {
+    div.with-toc {
+        margin-left:25vw;
+    }
+}
+
+@font-face {
+  font-family: 'Open Sans';
+  font-style: normal;
+  font-weight: 400;
+  font-stretch: 100%;
+  font-display: swap;
+  src: url(https://fonts.gstatic.com/s/opensans/v29/memSYaGs126MiZpBA-UvWbX2vVnXBbObj2OVZyOOSr4dVJWUgsjZ0B4gaVI.woff2) format('woff2');
+  unicode-range: U+0000-00FF, U+0131, U+0152-0153, U+02BB-02BC, U+02C6, U+02DA, U+02DC, U+2000-206F, U+2074, U+20AC, U+2122, U+2191, U+2193, U+2212, U+2215, U+FEFF, U+FFFD;
+}
+
+body, h1, h2, h3, h4, h5, h6, p, text {
+  font-family: "Open Sans", "Helvetica Neue", Helvetica, Arial, sans-serif !important;
+}

blueprint/src/macro/common.tex

@@ -0,0 +1,23 @@
+\theoremstyle{definition}
+
+\newtheorem{theorem}{Theorem}[chapter]
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{definition}[theorem]{Definition}
+
+\theoremstyle{remark}
+\newtheorem{remark}[theorem]{Remark}
+\newtheorem{remarks}[theorem]{Remarks}
+\newtheorem{example}[theorem]{Example}
+\newtheorem{examples}[theorem]{Examples}
+
+\setoperatorfont\mathsf
+
+% This is a workaround to make PlasTeX and XeLaTeX do the same thing: use the mathsf font for new operators.
+\newcommand{\newoperator}[1]{\operatorname{\mathsf{#1}}}
+
+\newcommand{\Con}{\newoperator{Con}}
+
+\newcommand{\NF}{\mathsf{NF}}
+\newcommand{\TTT}{\mathsf{TTT}}

blueprint/src/macro/print.tex

@@ -0,0 +1,7 @@
+\newcommand{\uses}[1]{}
+\newcommand{\proves}[1]{}
+\newcommand{\discussion}[1]{}
+\newcommand{\lean}[1]{}
+\newcommand{\leanok}{}
+\newcommand{\mathlibok}{}
+\newcommand{\notready}{}

blueprint/src/plastex.cfg

@@ -0,0 +1,18 @@
+[general]
+renderer=HTML5
+copy-theme-extras=yes
+plugins=leanblueprint
+
+[document]
+toc-depth=2
+toc-non-files=True
+
+[files]
+directory=../web/
+split-level=0
+
+[html5]
+localtoc-level=0
+extra-css=extra_styles.css
+mathjax-dollars=True
+theme=white

blueprint/src/print.tex

@@ -0,0 +1,51 @@
+% This file makes a printable version of the blueprint
+
+\documentclass{report}
+
+\usepackage[a4paper]{geometry}
+\usepackage{fontspec}
+\usepackage{unicode-math}
+\setmainfont[Path=../fonts/STIXTwo/,
+	UprightFont=*-Regular,
+	BoldFont=*-Bold,
+	ItalicFont=*-Italic,
+	BoldItalicFont=*-BoldItalic,
+	]{STIXTwoText}
+\setsansfont[Path=../fonts/Source_Sans_3/static/]{SourceSans3-Regular}[Ligatures={Common,TeX}]
+\setmathfont[Path=../fonts/STIXTwo/]{STIXTwoMath-Regular}
+\setmathfont[Path=../fonts/,range=\star]{TeXGyrePagellaMath}
+\setmonofont[Path=../fonts/,Scale=MatchLowercase]{FiraCode-Regular}
+
+\usepackage{xcolor}
+\usepackage{amsthm}
+\usepackage{hyperref}
+\usepackage{cleveref}
+% https://tex.stackexchange.com/a/81645
+\crefformat{section}{\S#2#1#3}
+\crefmultiformat{section}{\S\S#2#1#3}{ and~#2#1#3}{, #2#1#3}{, and~#2#1#3}
+
+\hypersetup{
+	colorlinks=true,
+	linkcolor=red!50!black,
+	citecolor=green!50!black,
+	urlcolor=magenta!70!black,
+}
+
+\input{macro/common}
+
+\input{macro/print}
+
+\title{New Foundations is consistent}
+\author{Sky Wilshaw}
+
+\begin{document}
+
+\maketitle
+
+\input{chapters/abstract.tex}
+
+\tableofcontents
+
+\input{content}
+
+\end{document}