Customizing leanblueprint

Stream: general

[Alex Brodbelt]

Hi,

I am using leanblueprint for my master's thesis project and over the next few weeks will be using it heavily and was hoping to use this thread to ask for some help, I hope that is ok:

The link to the blueprint is https://alexbrodbelt.github.io/ClassificationOfFiniteSubgroupsOfPGL/

1. I cannot get the mintedpackage to work. Things I have tried and were not sufficient:

• It seems \usepackage{minted} in both web.tex and print.tex is not sufficient.
• Downloaded the pygmentize for python
• Have considered downloading the minted.sty from https://github.com/leanprover/tutorial/blob/master/minted.sty but I'm not sure where to place such a file as the leanblueprint is not the typical LaTeX setup I have, if this makes sense.

2. How hard would it be to define a code environment similar to the proof environment that toggles between showing the minted environment showing the corresponding lean code for a proof/definition. Ideally I would put it below the proof, as I would like to have the following structure for a given theorem:

• informal statement
• formal statement
• informal proof
• formal proof
• comments on formalization

3. In general, defining another toggle environment would be quite useful or even new environments where the background is a different colours to emphasize it is code or not my work. My attempts so far have broken the blueprint.

I would appreciate any pointers or things I should bear in mind. Thank you for your patience :-)

[Patrick Massot]

Currently there is not minted support in plastex. But using pygmentize would be fairly easy since it’s also python.

[Patrick Massot]

You cannot hope plastex will swallow the original minted.sty. Implementing this in python directly will be much easier.

[Patrick Massot]

The listings support in plasTeX uses pygments, see https://github.com/plastex/plastex/blob/master/plasTeX/Packages/listings.py

[Patrick Massot]

By the way, do you also seek to produce a pdf version, or would you be happy with a web only rendering?

[Alex Brodbelt]

My supervisor is trying to bargain being able to submit the web version as it is much nicer. But so far the pdf renders very nicely anyway. Would using the listings package break the pdf?

[Patrick Massot]

About point 2, how do you want plasTeX to get the Lean code? Do you want to paste it into your TeX file? If yes then doing the toggle thing will be very easy. If you want to put a file path or url into the TeX file then it would take a bit more work. But everything is doable of course. You can hook the full power of python anywhere in the process.

[Alex Brodbelt]

I suspect doing \usepackage{listings} is sufficient as plasTeX can find a suitable script?

[Patrick Massot]

If you are happy to use listings for the pdf then yes. But if you want minted for the pdf and listings for the web version then you need to define an environment (called code of whatever) in both preambles (web.tex and print.tex) and then use your environment. So it’s a bit more work, but not much.

[Alex Brodbelt]

Patrick Massot said:

About point 2, how do you want plasTeX to get the Lean code? Do you want to paste it into your TeX file? If yes then doing the toggle thing will be very easy. If you want to put a file path or url into the TeX file then it would take a bit more work. But everything is doable of course. You can hook the full power of python anywhere in the process.

My plan was to copy and paste the relevant code into the TeX file, as I have 2 weeks and a half to clean up the project and present it.

[Alex Brodbelt]

In the future I would like to use python to automate more of this and maybe contribute to leanblueprint should it be of value, but for now it will have to do.

[Alex Brodbelt]

Patrick Massot said:

If you are happy to use listings for the pdf then yes. But if you want minted for the pdf and listings for the web version then you need to define an environment (called code of whatever) in both preambles (web.tex and print.tex) and then use your environment. So it’s a bit more work, but not much.

I see that makes sense. OK, so minted will work for the pdf.

[Patrick Massot]

Did you look at the code at https://github.com/PatrickMassot/plastexshowmore/ already?

[Alex Brodbelt]

I was not aware of this repo. I will check it out, thanks!

[Patrick Massot]

This is a pretty simple plasTeX plugin that add the icons showing and hiding proofs in certain blueprints. You can see those icons in the lower right corner of https://leanprover-community.github.io/sphere-eversion/blueprint/chap-local.html for instance.

[Patrick Massot]

Of course you need to read https://plastex.github.io/plastex/plastex/sec-plugins.html before making sense of any plasTeX plugin.

[Patrick Massot]

I mean this page and the following ones in the same section.

[Patrick Massot]

Another useful read is the theorem template at https://github.com/plastex/plastex/blob/master/plasTeX/Renderers/HTML5/Thms.jinja2s

[Alex Brodbelt]

This is extremely helpful, thank you Patrick!

[Patrick Massot]

As a case study in how things fit together, let’s try for instance to answer the question: “How does the LeanBlueprint plasTeX plugin manages to add a checkmark to formalized lemmas?” In the Thms.jinja2s, we see starting on line 27

    {% if doc.userdata['thm_header_extras_tpl'] %}
    <div class="thm_header_extras">
    {% for tpl in doc.userdata['thm_header_extras_tpl'] %}
    {% include tpl %}
    {% endfor %}
    </div>
    {% endif %}

and in https://github.com/PatrickMassot/leanblueprint/blob/master/leanblueprint/Packages/blueprint.py we see

CHECKMARK_TPL = Template("""
    {% if obj.userdata.leanok and ('proved_by' not in obj.userdata or obj.userdata.proved_by.userdata.leanok ) %}
    ✓
    {% endif %}
""")

and then further down

    document.userdata.setdefault(
        'thm_header_extras_tpl', []).extend([CHECKMARK_TPL])

Does it make some sense?

[Alex Brodbelt]

yes, this reminds me a fair bit of how things in svelte work.

[Alex Brodbelt]

what is tpl iterating over? What sort of data?

[Alex Brodbelt]

I suppose my initial questions without having read the sources you provide are: how do you link this back to the TeX or the web/print generation? I was looking at FLT and LeanAPAP to see how python scripts are used. Will think about this when I get back home, thank you Patrick :-)

[Alex Brodbelt]

Alex Brodbelt said:

what is tpl iterating over? What sort of data?

probably not a meaningful question, can probably figure this out.

[Patrick Massot]

Sorry, I was having dinner. It’s iterating over Jinja2 templates.

[Alex Brodbelt]

For others wanting to do similar, the verbatim package works very well with leanblueprint in both web and print version; it even renders the unicode! (or at least the subset of unicode I have thrown at it so far)

I tried listingsfor the web version and ran into issues with unicode and just setting it up in general.

I also tried minted for the print version and I suspect it would work well but it has issues rendering unicode - I did not try using inputenc to remedy this.

[Eric Wieser]

I think I have a minted implementation for plasTeX lying around somewhere...

[Alex Brodbelt]

I assume that when using a theorem from mathlib there is no way you can reference it using lean{} as it is not part of your project but part of mathlib?

The purpose of wanting to do this, is to help others wanting to use this particular part of mathlib understand how informal maths corresponds to formal maths and as far as I understand why certain decisions were made.

[Patrick Massot]

There should be no problem at all, unless I misunderstand the question.

[Eric Wieser]

Eric Wieser said:

I think I have a minted implementation for plasTeX lying around somewhere...

Presented without warranty:

from pathlib import Path
from plasTeX import Command, Environment, VerbatimEnvironment
from plasTeX.Base.LaTeX.Verbatim import verbatim, verb
from plasTeX.Logging import getLogger
from plasTeX.PackageResource import PackagePreCleanupCB, PackageCss
from plasTeX.PackageResource import PackageResource, PackageCss, PackageTemplateDir
from pygments import lexers
from pygments.formatters import HtmlFormatter
from pygments.lexers.special import TextLexer
import pygments
import textwrap

log = getLogger()

class minted(verbatim):
    autogobble = True
    language = ''
    def digest(self, tokens):
        verbatim.digest(self, tokens)
        text = self.textContent
        if self.autogobble:
            text = textwrap.dedent(text.lstrip('\n'))
        self.raw_content = text
        try:
            lexer = lexers.get_lexer_by_name(self.language)
        except Exception:
            log.warning(f"No lexer for {self.language}")
            lexer = TextLexer()
        self.html_listing = pygments.highlight(self.raw_content, lexer,
                HtmlFormatter(nowrap=True)).strip()

class mintinline(verb):
    language = ''
    def digest(self, tokens):
        verb.digest(self, tokens)
        text = self.textContent
        self.raw_content = text
        try:
            lexer = lexers.get_lexer_by_name(self.language)
        except Exception:
            log.warning(f"No lexer for {self.language}")
            lexer = TextLexer()
        self.html_listing = pygments.highlight(self.raw_content, lexer,
                HtmlFormatter(nowrap=True)).strip()


class lean(mintinline):
    language = 'lean'

class leanf(mintinline):
    language = 'lean4'

class leancode(minted):
    language = 'lean'

class lean4code(minted):
    language = 'lean4'
def ProcessOptions(options, document):

    tpl = PackageTemplateDir(
        renderers='html5',
        path=Path(__file__).parent/'templates')

    document.addPackageResource([tpl])

    cb = PackagePreCleanupCB(renderers='html5', data=make_pygments_css)
    css = PackageCss(renderers='html5', path=Path('pygments.css'))
    css.copy = False
    document.addPackageResource([
        cb, css,
        PackageCss(renderers='html5', path=Path(__file__).parent/'css'/'codeboxes.css')
    ])

def make_pygments_css(document):
    path = Path('styles')/'pygments.css'
    path.write_text(HtmlFormatter().get_style_defs())
    return [str(path)]

[Alex Brodbelt]

So I tried, putting \lean{Subgroup.center} to have the definition for the center visible but it does not find it and lists the definitions I have made as potential remedies.

image.png

[Alex Brodbelt]

Alex Brodbelt said:

For others wanting to do similar, the verbatim package works very well with leanblueprint in both web and print version; it even renders the unicode! (or at least the subset of unicode I have thrown at it so far)

I tried listingsfor the web version and ran into issues with unicode and just setting it up in general.

I also tried minted for the print version and I suspect it would work well but it has issues rendering unicode - I did not try using inputenc to remedy this.

It seems I got a bit excited, it does indeed work for the local web version - but when I push to github things fall apart. I wonder if this means I should modify what github actions run?
I suspect it is the unicode characters which XeTeX is not happy with

[Eric Wieser]

Unicode shouldn't be an issue for plasTeX (the blueprint software) or XeTeX

[Alex Brodbelt]

I get a combination of the following type warnings:

Package hyperref Warning: Token not allowed in a PDF string (Unicode):
(hyperref)                removing `math shift' on input line 1.

My hunch for this is that writing mathmode in the section titles does not make LaTeX hyperref happy - but it has not crashed because of this before.

and warnings from what I am guessing are the verbatim boxes:

Missing character: There is no ∃ (U+2203) in font [lmmono10-regular]:!

Overall, this leads to the following error message

! Internal error: bad native font flag in `map_char_to_glyph'

xdvipdfmx:fatal: File ended prematurely

In the larger trace at:
https://github.com/AlexBrodbelt/ClassificationOfFiniteSubgroupsOfPGL/actions/runs/13544289543/job/37852134797

Upon StackOverflow-ing: https://tex.stackexchange.com/questions/63244/internal-error-bad-native-font-flag-xelatex-fontspec-newtxmath-libertine

Maybe using \texttt{}is not a good idea for inline code? As it mixes OpenType and TFM fonts which is not supported in XeTeX.

Conclusion: I am not sure how to debug yet, maybe using your minted plasTeX should make my problems vanish?

[Patrick Massot]

All those error messages seem to have nothing to do with plastex.

[Patrick Massot]

They all come from xelatex.

[Patrick Massot]

And that mention of xdvipdfmx sounds very wrong. How could the dvi file format be involved in 2025?

[Patrick Massot]

And if it works locally then the issue is with the TeX setup in CI.

[Alex Brodbelt]

Ahhh so it indeed might be a problem with the CI?

[Eric Wieser]

Missing character: There is no ∃ (U+2203) in font [lmmono10-regular]:!

I would hope you can fix this by using a better font. Julia Mono is a reasonable choice, as is Deja Vu Sans Mono

[Alex Brodbelt]

I must admit I do not know too much about typesetting and LaTeX - I am guessing you mean I should fix the preamble to be (in some appropriate place):

\usepackage{fontspec}

\setmainfont{DejaVu Serif}

[Eric Wieser]

See #general > LaTeX beamer @ 💬 for an example with LuaLaTeX, which should be similar enough

[Alex Brodbelt]

(deleted)

[Alex Brodbelt]

(deleted)

[Alex Brodbelt]

Is there a reason why the dependency graph is not visible if one opens the html file from the web folder? Is there something I can do to make the dependency graph visible - it would be a shame if I could not show such a pretty thing!

(I should say that when I run leanblueprint web and then leanblueprint serve everything works wonderfully (aside from the bibliography being shy)

image.png

[Ruben Van de Velde]

Probably if that worked, the blueprint could also read all your passwords

[Alex Brodbelt]

I see

[Kevin Buzzard]

I'm assuming from the deleted messages and the screenshot that you now have things working! :-)

[Alex Brodbelt]

ehh, unfortunately that is not the case :'( - but I am cutting my losses :light_bulb:

[Mario Carneiro]

yeah, this is a general web browser limitation done for security reasons. You can work around it by serving the folder on localhost so that the browser applies a different security policy. A long time ago someone taught me that python supports this out of the box with python3 -m http.server, even without writing a line of python. But it sounds like leanblueprint serve also does the same thing

[Alex Brodbelt]

Ah so I can tell the markers to launch it using python3 -m ... so they can see the dependency graph? It's going to be interesting to see how they mark this Lean project...

[Alex Brodbelt]

Is there a way for using labels that don't appear in the dependency graph? (i.e theorems are already in mathlib but still want to reference)

[Eric Wieser]

Or you host the output on a (private) GitHub repo, which runs the server for you

[Eric Wieser]

Private repos still have public webpages, so you can just give the graders the url

[Ruben Van de Velde]

They might want a copy that can't be changed out from under them, though