feat: allow statements of theorems in 1000.yaml by grunweg · Pull Request #577 · leanprover-community/leanprover-community.github.io

grunweg · 2025-01-17T13:21:55Z

And display these on the generated webpage as well.

I don't expect the list of theorems with just a statement to grow large, but for some results, this could be useful.
Accompanies leanprover-community/mathlib4#20637; it's better to merge this PR first.

grunweg · 2025-01-17T13:22:54Z

@bryangingechen Would you like to take a look? The first commit is very easy; I could drop the second one if you prefer.

I cannot test this locally (sadly) and had some ... fun merging this, so testing locally could be helpful. Thanks!

make_site.py

grunweg · 2025-01-18T10:24:57Z

Thanks for the careful review! I think this is ready again.
I tested this locally (by commenting everything that doesn't work on my part, which is not this section): it runs without errors.

bryangingechen

This builds locally for me now too. Let's add the stuff about formalized statements to the 100 theorems pages and then we can merge.

templates/1000-missing.html

templates/100.html

bryangingechen · 2025-01-18T13:27:46Z

Thanks!

robertylewis · 2025-01-19T17:11:28Z

@grunweg @bryangingechen The scheduled website build failed last night with this log. (I don't know why the failure emails come to me or whether they come to other people too...)

Rendering 1000-missing.html...
Traceback (most recent call last):
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/staticjinja/staticjinja.py", line 377, in render_template
Downloading header-data.json...
    rule = self.get_rule(template.name)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/staticjinja/staticjinja.py", line [29](https://github.com/leanprover-community/leanprover-community.github.io/actions/runs/12850171819/job/35829553224#step:6:30)2, in get_rule
    raise ValueError("no matching rule")
ValueError: no matching rule

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/./make_site.py", line 862, in <module>
    render_site(ROOT/'build', base_url, reloader='--reload' in sys.argv, only=only)
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/./make_site.py", line 851, in render_site
    site.render(use_reloader=reloader)
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/staticjinja/staticjinja.py", line 4[34](https://github.com/leanprover-community/leanprover-community.github.io/actions/runs/12850171819/job/35829553224#step:6:35), in render
    self.render_templates(self.templates)
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/staticjinja/staticjinja.py", line 393, in render_templates
    self.render_template(template)
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/staticjinja/staticjinja.py", line [38](https://github.com/leanprover-community/leanprover-community.github.io/actions/runs/12850171819/job/35829553224#step:6:39)2, in render_template
    template.stream(**context).dump(filepath, self.encoding)
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/jinja2/environment.py", line 1623, in dump
    real_fp.writelines(iterable)
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/jinja2/environment.py", line 1618, in <genexpr>
    iterable = (x.encode(encoding, errors) for x in self)  # type: ignore
Downloaded.
Parsing header-data.json...
Parsed.
Error: 1000+ theorems entry Q776578 refers to a nonexistent declaration isSemisimpleRing_iff_pi_matrix_divisionRing
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/jinja2/environment.py", line 1667, in __next__
    return self._next()  # type: ignore
           ^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/jinja2/environment.py", line 1348, in generate
    yield self.environment.handle_exception()
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/jinja2/environment.py", line 9[42](https://github.com/leanprover-community/leanprover-community.github.io/actions/runs/12850171819/job/35829553224#step:6:43), in handle_exception
    raise rewrite_traceback_stack(source=source)
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/templates/1000-missing.html", line 1, in top-level template code
    {% extends '_base.html' %}
    ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/templates/_base.html", line 50, in top-level template code
    {% block content %}
^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/templates/1000-missing.html", line 4, in block 'content'
    {% markdown %}
    ^^^^^^^^^^^^^^^
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/./make_site.py", line 86, in _markdown_support
    return self.environment.markdowner.render(Document(caller())).strip()
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/mistletoe/base_renderer.py", line 94, in render
    return self.render_map[token.__class__.__name__](token)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/mistletoe/html_renderer.py", line 201, in render_document
    inner = '\n'.join([self.render(child) for child in token.children])
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x[64](https://github.com/leanprover-community/leanprover-community.github.io/actions/runs/12850171819/job/35829553224#step:6:65)/lib/python3.11/site-packages/mistletoe/html_renderer.py", line 201, in <listcomp>
    inner = '\n'.join([self.render(child) for child in token.children])
                       ^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.11.11/x64/lib/python3.11/site-packages/mistletoe/base_renderer.py", line 94, in render
    return self.render_map[token.__class__.__name__](token)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/runner/work/leanprover-community.github.io/leanprover-community.github.io/mistletoe_renderer.py", line 107, in render_block_code
    code = replace_math(token.children[0].content, self.math)
                                                   ^^^^^^^^^
AttributeError: 'CustomHTMLRenderer' object has no attribute 'math'

bryangingechen · 2025-01-19T17:12:54Z

Strange, I wish I would get them, but I don't... @grunweg can you take a look?

grunweg added 2 commits January 17, 2025 14:18

chore: allow mere *statements* of 1000+ theorems

266396c

chore: show 1000+ theorems with formalised statements separately

08f6aec

grunweg mentioned this pull request Jan 17, 2025

[Merged by Bors] - feat(1000.yaml): allow statements of theorems also leanprover-community/mathlib4#20637

Closed

2 tasks

bryangingechen self-assigned this Jan 17, 2025

bryangingechen reviewed Jan 17, 2025

View reviewed changes

make_site.py Outdated Show resolved Hide resolved

make_site.py Show resolved Hide resolved

make_site.py Outdated Show resolved Hide resolved

make_site.py Outdated Show resolved Hide resolved

Address review comments

34f9694

bryangingechen reviewed Jan 18, 2025

View reviewed changes

templates/1000-missing.html Outdated Show resolved Hide resolved

templates/100.html Outdated Show resolved Hide resolved

grunweg added 2 commits January 18, 2025 14:06

Add the same comment to 100{-missing}.html.

e7d7481

Add statements also

307737e

bryangingechen merged commit 6c6e802 into leanprover-community:lean4 Jan 18, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: allow statements of theorems in 1000.yaml#577

feat: allow statements of theorems in 1000.yaml#577
bryangingechen merged 5 commits intoleanprover-community:lean4from
grunweg:MR-allow-statements

grunweg commented Jan 17, 2025

Uh oh!

grunweg commented Jan 17, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jan 18, 2025 •

edited

Loading

Uh oh!

bryangingechen left a comment

Uh oh!

Uh oh!

Uh oh!

bryangingechen commented Jan 18, 2025

Uh oh!

robertylewis commented Jan 19, 2025

Uh oh!

bryangingechen commented Jan 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

grunweg commented Jan 17, 2025

Uh oh!

grunweg commented Jan 17, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jan 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

bryangingechen commented Jan 18, 2025

Uh oh!

robertylewis commented Jan 19, 2025

Uh oh!

bryangingechen commented Jan 19, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

grunweg commented Jan 18, 2025 •

edited

Loading