[Merged by Bors] - feat: add a file tracking results from the 1000+ theorems project#19634
[Merged by Bors] - feat: add a file tracking results from the 1000+ theorems project#19634
Conversation
PR summary d61e514b58Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
|
The new file seems to be in a random order. Since this project doesn't have a fixed order (theorem 1, theorem 2, ...), I'd suggest sorting it either alphabetically by theorem name (whether by Unicode collation or code-point order) or numerically by Wikidata code. (The 1000-plus data includes MSC codes, and use of those would be reasonable to provide more structure in the list on our website rather than having a purely alphabetical list there, but I'm not sure if sorting by MSC code would make so much sense for this source file.) |
|
Good catch! You were right (the old file depended on file system order in some sense); I've added sorting by wikidata ID now. |
|
Some of the titles contain unicode-escapes, e.g. |
That's added by the yaml generation script. I'll see if there's an option to output unicode instead. |
Extracted from #19634.
Generate 1000.json during the build, and check its well-formedness. And document yaml_check.py slightly better.
3bdbf3c to
d1f62d7
Compare
d1f62d7 to
623063d
Compare
|
Updated and rebased now. This is ready for review again. |
|
For cross-reference: 1000-plus/1000-plus.github.io#6 and 1000-plus/1000-plus.github.io#7. |
|
Thanks! |
|
bors merge |
…9634) Add a new file `1000.yaml`, tracking the formalisation status of theorems from the [1000+ theorems project](https://1000-plus.github.io). Make `check-yaml` handle this file also. Future PRs will - expose this information on the webpage - add infrastructure for synchronising this file with the upstream repository - could add an attribute similar to the `stacks` attribute, and generate this file from the tagging - add information on existing formalisation projects in Lean.
|
Pull request successfully merged into master. Build succeeded: |
Add a new file
1000.yaml, tracking the formalisation status of theoremsfrom the 1000+ theorems project. Make
check-yamlhandle this file also.Future PRs will
stacksattribute, and generate this file from the tagging