[Merged by Bors] - ci: basic check on fields in 100.yaml and 1000.yaml by bryangingechen · Pull Request #20078 · leanprover-community/mathlib4

bryangingechen · 2024-12-19T16:22:23Z

This PR makes scripts/yaml_check.py verify that 100.yaml and 1000.yaml only contain fields the webpage expects them to. Otherwise, changes in mathlib breaking the website won't be noticed until they are merged; this has happened several times in the last days. In particular, replace two occurrences of note in 1000.yaml by comment.
To this end, this PR copies the dataclass constructors which are used in the website script to scripts/yaml_check.py (along with a comment asking to keep them in sync).

While at it, this PR documents the fields in 100.yaml as well, and moves the documentation for 1000.yaml to the copied dataclasses in yaml_check.py.

In addition, validate that at most one of the fields decl and decls are passed: the webpage also does this; this avoids late surprises.

Co-authored-by: grunweg rothgang@math.uni-bonn.de

After merging this, the website will be broken until leanprover-community/leanprover-community.github.io#563 is merged.

docs/100.yaml

github-actions · 2024-12-19T16:23:13Z

PR summary 3c3fb6a999

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ HundredTheorem:
+ ThousandPlusTheorem:

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg

Looks good so far. I need to run now, perhaps I can provide a doc-string for doc_decls later.

docs/100.yaml

scripts/yaml_check.py

bryangingechen · 2024-12-19T18:08:03Z

Thanks for the quick review! I've marked this as awaiting-author until @grunweg has had a chance to add info about doc_decls (and perhaps any other changes to the docstrings). In the meantime I'll consider adding the decl vs decls check as well.

grunweg

Actually, one more thought: there are now two locations for these doc comments on the respective fields: once in {100,1000}.yaml, and once in the HundredTheorems class.

At the minimum, can we make sure to copy all the doc comments everywhere, and add comments to keep these in sync? In fact, I wonder if it's better to shorten the comment in the yaml file, referring to yaml_check.py for a documentation of the respective fields.

(I seemingly cannot edit your PR, so haven't pushed any of these changes directly.)

refer to yaml-check instead

grunweg · 2025-01-07T12:40:41Z

I just went ahead and updated this PR for the proposed webpage PR (and also added validation for decl vs decls).

The last commit (a more flexible date format) is in anticipation of 1000-plus/1000-plus.github.io#10.

grunweg · 2025-01-07T14:23:03Z

Merged master, fixed another violation of the file format and improved the error message. I would maintainer merge this now - but as I wrote the second half of the code, I'd prefer not to.

sync with leanprover-community/leanprover-community.github.io#563

grunweg · 2025-01-07T15:22:51Z

I'm not sure about the last commit: I consciously deleted those doc-comments, as they make no sense in the context of mathlib. What do you think?

bryangingechen · 2025-01-07T15:25:39Z

Ah, I just thought it'd be easier to keep them in sync if they were exactly the same text so I copied and pasted them without thinking. I guess it's not much more work to just copy and paste the fields though. Let me revert.

grunweg · 2025-01-07T15:32:25Z

I hope the allowed fields will change very rarely, if at all. (The current changes are bug fixes, in my opinion.)

bryangingechen · 2025-01-07T15:38:36Z

@fpvandoorn This PR has gone through major revision by @grunweg and should now be in sync with leanprover-community/leanprover-community.github.io#563. Do you mind re-reviewing / merging this if it looks good? After this is merged the website will be temporarily broken, but I plan on merging the PR over there in short order so there won't be any actual broken builds, hopefully.

fpvandoorn · 2025-01-09T12:56:39Z

Thanks!

bors merge

This PR makes `scripts/yaml_check.py` verify that `100.yaml` and `1000.yaml` only contain fields the webpage expects them to. Otherwise, changes in mathlib breaking the website won't be noticed until they are merged; this has happened several times in the last days. In particular, replace two occurrences of `note` in `1000.yaml` by `comment`. To this end, this PR copies the dataclass constructors which are used in the website script to `scripts/yaml_check.py` (along with a comment asking to keep them in sync). While at it, this PR documents the fields in `100.yaml` as well, and moves the documentation for `1000.yaml` to the copied dataclasses in `yaml_check.py`. In addition, validate that at most one of the fields `decl` and `decls` are passed: the webpage also does this; this avoids late surprises. Co-authored-by: grunweg <rothgang@math.uni-bonn.de> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-01-09T13:05:57Z

Pull request successfully merged into master.

Build succeeded:

bryangingechen added 4 commits December 19, 2024 10:55

ci: basic check on fields in 100.yaml and 1000.yaml

a7b982f

Merge remote-tracking branch 'origin/master' into bgc-yaml-check

971d2c9

remove duplicated url field

51d2bac

add / update documentation in 100.yaml+1000.yaml

4a39c30

bryangingechen requested review from fpvandoorn and grunweg December 19, 2024 16:22

bryangingechen commented Dec 19, 2024

View reviewed changes

docs/100.yaml Outdated Show resolved Hide resolved

bryangingechen mentioned this pull request Dec 19, 2024

remove duplicated field from ThousandPlusTheorem dataclass, add comments refering to scripts/yaml_check.py in mathlib4 leanprover-community/leanprover-community.github.io#561

Closed

bryangingechen added the CI Modifies the continuous integration setup or other automation label Dec 19, 2024

grunweg reviewed Dec 19, 2024

View reviewed changes

docs/100.yaml Outdated Show resolved Hide resolved

scripts/yaml_check.py Outdated Show resolved Hide resolved

fpvandoorn approved these changes Dec 19, 2024

View reviewed changes

bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 19, 2024

grunweg reviewed Dec 19, 2024

View reviewed changes

bryangingechen mentioned this pull request Jan 3, 2025

[Merged by Bors] - chore(1000): remove identifiers #20445

Closed

grunweg added 4 commits January 7, 2025 13:32

chore: update copy-pasted declarations from the webpage's 563

52b849d

doc: remove explicit documentation in 100.yaml and 1000.yaml,

2a79085

refer to yaml-check instead

feat: also verify that decl and decls are never specified together

3265094

chore: more flexible date

6069331

grunweg mentioned this pull request Jan 7, 2025

[Merged by Bors] - chore(1000.yaml): re-enable comments, add more entries #20554

Closed

grunweg added 3 commits January 7, 2025 15:20

fix(yaml_check.py): better error message

148dcb3

Merge branch 'master' into bgc-yaml-check

bc8f996

chore: fix file format

0abbb2c

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 7, 2025

bryangingechen mentioned this pull request Jan 7, 2025

refactor: distinguish data fields in the yaml files from the webpage template leanprover-community/leanprover-community.github.io#563

Merged

Update yaml_check.py

7b38b44

sync with leanprover-community/leanprover-community.github.io#563

revert docstring copy paste

3c3fb6a

bryangingechen requested a review from fpvandoorn January 7, 2025 15:36

bryangingechen mentioned this pull request Jan 7, 2025

fix(1000.yaml): remove wrong field 'note' #20555

Closed

ghost added the ready-to-merge This PR has been sent to bors. label Jan 9, 2025

mathlib-bors bot changed the title ~~ci: basic check on fields in 100.yaml and 1000.yaml~~ [Merged by Bors] - ci: basic check on fields in 100.yaml and 1000.yaml Jan 9, 2025

mathlib-bors bot closed this Jan 9, 2025

mathlib-bors bot deleted the bgc-yaml-check branch January 9, 2025 13:06

Conversation

bryangingechen commented Dec 19, 2024 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Dec 19, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3c3fb6a999

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

bryangingechen commented Dec 19, 2024

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg commented Jan 7, 2025

Uh oh!

grunweg commented Jan 7, 2025

Uh oh!

grunweg commented Jan 7, 2025

Uh oh!

bryangingechen commented Jan 7, 2025

Uh oh!

grunweg commented Jan 7, 2025

Uh oh!

bryangingechen commented Jan 7, 2025

Uh oh!

fpvandoorn commented Jan 9, 2025

Uh oh!

mathlib-bors bot commented Jan 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

bryangingechen commented Dec 19, 2024 •

edited by grunweg

Loading

github-actions bot commented Dec 19, 2024 •

edited

Loading

grunweg left a comment •

edited

Loading