refactor: distinguish data fields in the yaml files from the webpage template#563
Conversation
grunweg
force-pushed
the
MR-refactor-fields-strawman
branch
from
0d0e5d4 to
77c06c4
Compare
grunweg
force-pushed
the
MR-refactor-fields-strawman
branch
from
77c06c4 to
460953d
Compare
grunweg
changed the title
yaml files from the webpage template
This is another difference between 100.yaml and 1000.yaml. We choose to match the upstream field names; this is easy to do now.
|
Thanks for your review! I just saw this now (while I was pushing some additional commits). I'll incorporate it now. |
And make sure to mention that it is optional
|
I have addressed all comments. |
| url: Optional[str] = None | ||
| note: Optional[str] = None | ||
| # any additional notes or comments | ||
| comment: Optional[str] = None |
There was a problem hiding this comment.
This is causing my local tests of this PR to fail, so I have temporarily patched this out so I can keep checking things, but just to make sure, the idea is to merge leanprover-community/mathlib4#20078 (temporarily breaking the website), and then merge this PR?
There was a problem hiding this comment.
Oh right... I noticed a moment ago, but then forgot that 1000.yaml also contains some instances of note now...
I created leanprover-community/mathlib4#20555, which should allow landing this PR.
There was a problem hiding this comment.
In general, I'm not sure what the standard for "no changes breaking the webpage" is: given that the procedure so far has been somewhat permissive with "if the website breaks just once, that's ok", I'm fine with putting in some effort to avoid intermediate broken states - but bending over backwards seems a bit out of proportion.
There was a problem hiding this comment.
Ah, I maybe should have said this up front, but I'm personally also fine with having the website be temporarily broken while we coordinate efforts between repos. Sorry to make you go through the effort, but to keep the process simple, let's close leanprover-community/mathlib4#20555 and focus on getting someone (Floris?) to merge leanprover-community/mathlib4#20078 (which looks about done to me) and once that's in, I'll try and merge this immediately so there's no actual downtime.
bryangingechen
left a comment
bryangingechen
left a comment
There was a problem hiding this comment.
I've just synced the dataclasses to leanprover-community/mathlib4#20078 via copy-paste and realized that we should have corresponding comments here as well:
Co-authored-by: Bryan Gin-ge Chen <[email protected]>
bryangingechen
left a comment
bryangingechen
left a comment
There was a problem hiding this comment.
This now works locally (modulo a temporary patch to the comment field, which will become unncessary once leanprover-community/mathlib4#20078 is merged).
As mentioned above, I plan to merge this once that PR is in to avoid website downtime.
|
LGTM I'm happy to merge, but maybe it's better to wait until the Mathlib PR has actually been merged into master? |
|
The mathlib PR has been merged now. |
|
The build is failing, but I think it's just because doc-gen hasn't run yet (and hence we still have an old version of the yaml files). Let me re-trigger a docs build and then see if the website gets fixed. |
|
Right. I wonder why leanprover-community/mathlib4#20078 didn't cover this... but leanprover-community/mathlib4#20554 does include the fix now. |
|
Ah, looks like #20078 doesn't actually cause the build to fail when an error is detected: https://github.com/leanprover-community/mathlib4/actions/runs/12690334474/job/35370960547#step:19:8 I've submitted a fix at leanprover-community/mathlib4#20614 |
|
After retriggering the docs build once again, the website build finally succeeded! Everything looks OK at first glance... |
|
There is one bug: the count in 1000.yaml is wrong --- is only counts theorems with an author; it should count theorems with either an author, or a |
|
The same filter should be applied in 1000-missing.html. |
3 participants
Currently,
{Hundred,ThousandPlus}Theoremmix data for two different purposes:decl{s}fields contain the parsed declarations from the yaml filedoc_declsfields contains the source code for the corresponding generated documentationMake this distinction clearer by introducing a new class for theorems on the webpage: this allows omitting the
declsfield, and containsdoc_declsinstead. This will allow for stronger validation of theyamlfiles in mathlib. It also provides a shared abstraction between100.yamland1000.yaml.While at it, we also
{Hundred,ThousandPlus}Theoremcommentfield in1000.yaml(this is a pre-existing bug, which [Merged by Bors] - chore(1000): remove nonexistent fields mathlib4#20493 found)