Skip to content

feat: Add PhyslibAlpha to TODO items#1204

Open
jstoobysmith wants to merge 3 commits into
leanprover-community:masterfrom
jstoobysmith:TODOForPhyslibAlpha
Open

feat: Add PhyslibAlpha to TODO items#1204
jstoobysmith wants to merge 3 commits into
leanprover-community:masterfrom
jstoobysmith:TODOForPhyslibAlpha

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Made using Claude Opus 4.8. Though the changes here are minor.

Adds PhyslibAlpha to the TODO item collection, making sure that they appear in the TODO list.

claude and others added 2 commits June 18, 2026 06:04
Import `PhyslibAlpha` in `TODO_to_yml`'s `main` so that `TODO "..."`
items declared in PhyslibAlpha files are collected into `docs/_data/TODO.yml`.

Normalise the `PhyslibAlpha.` prefix to `Physlib.` in
`PhyslibCategory.ofFileName` so PhyslibAlpha items are categorised by
physics topic in the same way as their Physlib counterparts.

Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Jr1KNVgo8ZWE6pbd9vJvL7
Support PhyslibAlpha module categorization in TODO generator
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@morrison-daniel

Copy link
Copy Markdown
Collaborator

I think it would be good to separate PhyslibAlpha TODOs from the rest. Probably making one category for all of PhyslibAlpha is sufficient since the idea of PhyslibAlpha is to be low impact on maintenance and I foresee fewer TODOs as stuff will be added "as is".

@jstoobysmith jstoobysmith requested a review from zhikaip June 19, 2026 05:42
@jstoobysmith

Copy link
Copy Markdown
Member Author

@morrison-daniel Sounds good, will make this change now.

@zhikaip zhikaip left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. but honestly before I looked at this I thought this would be saying upstreaming physlibalpha to physlib as a todo, maybe there should be a mechanism that we should also think about for a process to do so

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants