Conversation
`os.killpg` does not exist on Windows, so the first per-module timeout in `rm_set_option.py` raised `AttributeError` and left the build running. Add a `_kill_tree` helper that falls back to `taskkill /F /T`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to Zulip and join the Lean community. |
PR summary 9c320c48edImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
os.killpgdoes not exist on Windows, so the first per-module timeout inrm_set_option.pyraisedAttributeErrorand left the build running. Add a_kill_treehelper that falls back totaskkill /F /T.Found and tested by running
rm_set_option.pyon Physlib (leanprover-community/physlib#1705), where the run then completed.Disclaimer: I encountered this while running the script on Physlib using a windows PC, and Claude suggested this fix for me which I think may be useful to upstream.