chore: sync rm_set_option with mathlib, fix it on Windows, remove 29 respectTransparency options - #1705
Conversation
…thlib (#41997) Skip `set_option` lines preceded by a `--` or `/- ... -/` comment, and add `backward.isDefEq.respectTransparency.types` to the default options. Co-authored-by: Claude Opus 5.5 <no-reply+claude-opus-5-5@anthropic.com>
`os.killpg` does not exist on Windows, so the first per-module timeout crashed `rm_set_option.py` and left the build running. Add a `_kill_tree` helper that falls back to `taskkill /F /T`. Co-authored-by: Claude Opus 5.5 <no-reply+claude-opus-5-5@anthropic.com>
…ency false Found by `scripts/rm_set_option.py`: 29 lines in 8 files are no longer needed. Co-authored-by: Claude Opus 5.5 <no-reply+claude-opus-5-5@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
jstoobysmith
left a comment
There was a problem hiding this comment.
Looks good to me. Approved
This PR updates the
set_optionremoval script and runs it across the repo.Commits
chore(scripts): sync rm_set_option.py and set_option_utils.py with mathlib. Brings in mathlib4#41997:set_optionline alone if the line above is a--comment or ends in-/.backward.isDefEq.respectTransparency.typesis added to the default options.fix(scripts): kill timed-out builds on Windows in dag_traversal.py.os.killpgdoesn't exist on Windows, so the first per-module timeout crashed the script and left the build running. A new_kill_treehelper falls back totaskkill /F /T. This is a local change to a file copied from mathlib; I plan to send it upstream too.chore: remove unnecessary set_option backward.isDefEq.respectTransparency false. The script's results: 29 lines removed in 8 files.Relativity/PauliMatrices/ToTensor.leanSpaceAndTime/SpaceTime/Basic.leanRelativity/Special/TwinParadox/Basic.leanElectromagnetism/Distributional/Dynamics/IsExtrema.leanElectromagnetism/Distributional/FieldStrength.leanRelativity/LorentzGroup/Boosts/Generalized.leanRelativity/LorentzGroup/Rotations.leanQuantumInfo/Entropy/VonNeumann.leanNo lemmas or definitions are added or removed.
Reviewer map: commits 1 and 2 are small script diffs. Commit 3 only deletes
set_optionlines and can be skimmed. Of the 659 lines tried across 178 files, 630 are still needed.🤖 Generated with Claude Code