search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
53 stars 122 forks source link

`{{` cannot be used in markdown files #168

Open bryangingechen opened 3 years ago

bryangingechen commented 3 years ago

We're telling staticjinja that every .md file is a jinja2 template, so if one of them contains {{ (e.g. when talking about "weakly implicit" arguments in Lean, (usually written ⦃ in unicode)), jinja2 will be unable to parse the file and then complain:

jinja2.exceptions.TemplateSyntaxError: unexpected char 'XX' at YY

This came up when testing templates/latex.md in #165.

robertylewis commented 3 years ago

Are we using this feature at all? It looks like all our jinja2 templates are .html files, but I'm not sure. Also I have no idea how to disable this processing on markdown files. So this isn't a very helpful question...

bryangingechen commented 3 years ago

I agree that we're not actually using the markdown files as templates, and I tried to figure out how to disable the checking but it seemed like it would require a bigger refactor, so I didn't dig too hard.

I did a search just now and we do actually have {{ in ci.md inside a yaml code block: 

          repo: ${{ github.repository }}
          access-token: ${{ secrets.GITHUB_TOKEN }}

and contribute/doc.md inside a Lean code block:

| binder_info.strict_implicit := ("{{", "}}")

So this may be less of a big deal than I thought. In the example that was breaking, {{ was in one of the LaTeX tests that wasn't in a code block and jinja complained, so I changed it to { {.