feat(CI): handle multi-part Erdős problems in status check#2327
feat(CI): handle multi-part Erdős problems in status check#2327zond wants to merge 2 commits intogoogle-deepmind:mainfrom
Conversation
For problems with no single `erdos_{N}` theorem (e.g. multi-part problems
with `erdos_{N}.parts.i`, `erdos_{N}_cycles`, etc.), collect all non-variant
theorems and report open if any part is open.
|
I'd like to have @danielchin's opinion here! |
|
I agree that we probably need to come up with a proper standard and document it in the README since it looks like the naming convention has evolved over time. I'll call the two potential parts of an Erdos problem: the main part (whatever is in the red or green box) and the additional text (whatever is below the red or green box). For the additional text, I think this is easy. We just always call it For the main part, we have to consider all the types of questions we have and whatever future ones T. Bloom might add in the future.
Assuming that we're okay with that naming convention, we can just check for all I did previously ask something similar to this in the Zulip chat: #Formal conjectures > Referencing OEIS @ 💬 Yael mentioned that we should replace the |
| def is_variant(suffix): | ||
| """Check if a theorem name suffix indicates a variant (not a main part).""" | ||
| # ".variants." anywhere in the suffix means it's a variant | ||
| return ".variants." in suffix or ".variant." in suffix |
There was a problem hiding this comment.
Can you leave a TODO here (you can assign it to me) to remove anything that's variant. We should just rename everything to variants and have the linter catch anything that's not one of our existing patterns.
|
Sounds good, @danielchin! We could add this naming convention to a README.md in |
|
Yup, I can do the write up and then do a massive clean up to ensure standards are being met. Feel free to assign me an issue. |
|
So, do I need to change anything with this PR, or? |
|
You can drop the condition on |
3 participants
For problems with no single
erdos_{N}theorem (e.g. multi-part problems witherdos_{N}.parts.i,erdos_{N}_cycles, etc.), collect all non-variant theorems and report open if any part is open.