Tutorial: Getting Started with Blueprint-Driven Projects

Stream: general

[Pietro Monticone]

Hi everyone,

I am pleased to announce the public release of the video recording of my tutorial talk, presented to one of our working groups at the Hausdorff Research Institute for Mathematics in Bonn.

This talk was designed for mathematicians at all levels, from students to professors, from enthusiasts to professional researchers. It aimed to provide a comprehensive introduction to the design, management, and implementation of blueprint-driven formalisation projects in Lean, with almost no prerequisite knowledge of Git, GitHub, continuous integration systems, and other technical tools.

You can watch the video here. All relevant references are available in the video description.

I hope you find the content clear and informative. I encourage you to test the template and the new LeanBlueprint and share your feedback. Your critical comments and suggestions are highly appreciated: they will be invaluable for improving these tools and for future formalisation projects in Lean that depend on them.

[Terence Tao]

It was a bit bumpy, but I was able (with @Pietro Monticone 's help) to get the template set up on a Windows machine (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Leanblueprint.20for.20Windows for a more detailed report). There do appear to be some speed bumps in the current installation instructions, so having more feedback of people actually trying out this template would be valuable.

[Bolton Bailey]

I found the installation worked pretty well on Mac (although I was also a bit confused, I hadn't realized I needed to install GraphViz for it to work). I am having a bit of trouble producing a valid content.tex file. Is it the case that I actually need to add \newtheorem{theorem}{Theorem} somewhere? Where do I do that?

[Pietro Monticone]

All the information gathered during the setup of @Terence Tao's project has been incorporated into the template README, which can be found here. Thank you very much!

[Pietro Monticone]

If you prefer not to post in this public thread, please feel free to send me a direct message. I am more than happy to assist you and learn from your user experience!

[Pietro Monticone]

Bolton Bailey said:

I was also a bit confused, I hadn't realized I needed to install GraphViz for it to work.

I noted it here, but I apologize for not making it clear enough.

[Terence Tao]

Bolton Bailey said:

I found the installation worked pretty well on Mac (although I was also a bit confused, I hadn't realized I needed to install GraphViz for it to work). I am having a bit of trouble producing a valid content.tex file. Is it the case that I actually need to add \newtheorem{theorem}{Theorem} somewhere? Where do I do that?

I put

\declaretheorem[numberwithin=chapter]{theorem}
\declaretheorem[sibling=theorem]{proposition}
\declaretheorem[sibling=theorem]{corollary}
\declaretheorem[sibling=theorem]{remark}
\declaretheorem[sibling=theorem]{lemma}
\declaretheorem[sibling=theorem]{definition}
\declaretheorem[sibling=theorem]{example}
\declaretheorem[sibling=theorem]{conjecture}

in macros/print.tex and

\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{sublemma}[theorem]{Sub-lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{conjecture}[theorem]{Conjecture}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

in macros/web.tex. I think I also needed to include amsthm or something in the main print.tex and web.tex files.

[Pietro Monticone]

Bolton Bailey said:

Is it the case that I actually need to add \newtheorem{theorem}{Theorem} somewhere? Where do I do that?

I have opened a PR for your project, adding typical theorem and definition environments in the macros/common.tex as usual. This includes those to be displayed in the blueprint dependency graph and those that are not.

Hope it helps.

[Pietro Monticone]

In the new version of the LeanProject template the "Customise this Template" section will be fully automated. I'm working on a simple script I'll push in a few minutes or so.

Sorry for the inconvenience.

[Pietro Monticone]

Done. You can find the new relevant instructions here.

[Bolton Bailey]

Thanks, here's another more general question I have about leanblueprint/latex after playing around with it.

I see that it is possible to write \label{Batched FRI error bound} in one of my theorems, and the blueprint renders this name fine in the graph and will allow it to be referenced by \uses. This is surprising in retrospect, since I thought \labels had to not have spaces. Is it possible to label things with a term without spaces and still have leanblueprint render it with spaces?

[Pietro Monticone]

Not without any changes in the LeanBlueprint package as far as I know.

[Patrick Massot]

I am a bit worried that Pietro’s nice template is fragmenting the documentation in a way that makes it harder to understand what needs to be done. I see many things in the discussion above that are addressed very explicitly in the official documentation.

[Patrick Massot]

I wonder whether I should include the \newtheorem lines in the blueprint template (here I mean the TeX templates that are used by leanblueprint new, not Pietro’s project template). There is a tension here. On one hand, there is a list of theorems environments that are included into the dependency graph by default (definition, lemma, proposition, theorem and corollary as explained in the documentation). On the other hand, we want to give freedom about that. For instance we see in Terence’s message that he chose to use the thmtools package instead of amsthm for the pdf version.

[Patrick Massot]

Probably the current emphasis on freedom is not consistent with the global goal of having something that works out of the box with reasonable default values. So I will probably modify the templates later today unless someone complains here.

[Patrick Massot]

Ok, I edited the templates and pushed a new version to pypi.

[Patrick Massot]

I forgot to answer Bolton’s question about labels. I think that spaces in labels names are a rather evil feature of LaTeX that is half supported by the ecosystem (independently of leanblueprint). So I would not recommend using them. But you may have collaborators who are addicted to them. Globally LaTeX is a very permissive language, and this creates a huge gray zone of semi-allowed things, much like with HTML. This creates a tension when working on leanblueprint. Spending a lot of time and code obfuscation in order to support LaTeX corner cases is not fun, and can seem very counter-productive. But habits are hard to change, especially for people who start using Lean after spending decades using LaTeX. And, more importantly, Lean blueprints can start their life as ordinary LaTeX files meant for ordinary publication. In that case spending a lot of time tweaking the LaTeX source to make it acceptable for the blueprint is also not fun and a waste of time.