-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor: tweak and move functionality for getting all modules out of scripts
#13339
Conversation
This PR/issue depends on:
|
7b84fa1
to
09c2feb
Compare
… scripts/ It is needed in other scripts: the easiest way to depend on this is to move this to mathlib. Better places are welcome!
09c2feb
to
629199e
Compare
This looks good to me! The rename of the variable should have really happened when I refactored the code, but I only noticed it now. Thanks! (I won't be at a computer until Monday, so I can't really test this code right now.) |
For the future, |
bors d+ |
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks for the quick review |
… `scripts` (#13339) With #13245, two scripts in `scripts` would like to use very similar information: move it to a central place instead (a file in `Mathlib/Util`). Suggestions for better locations are welcome! Also, split the `getAll` function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd. - [x] depends on: #11853 which adds these utility functions
Pull request successfully merged into master. Build succeeded: |
scripts
scripts
… `scripts` (#13339) With #13245, two scripts in `scripts` would like to use very similar information: move it to a central place instead (a file in `Mathlib/Util`). Suggestions for better locations are welcome! Also, split the `getAll` function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd. - [x] depends on: #11853 which adds these utility functions
… `scripts` (#13339) With #13245, two scripts in `scripts` would like to use very similar information: move it to a central place instead (a file in `Mathlib/Util`). Suggestions for better locations are welcome! Also, split the `getAll` function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd. - [x] depends on: #11853 which adds these utility functions
… `scripts` (#13339) With #13245, two scripts in `scripts` would like to use very similar information: move it to a central place instead (a file in `Mathlib/Util`). Suggestions for better locations are welcome! Also, split the `getAll` function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd. - [x] depends on: #11853 which adds these utility functions
With #13245, two scripts in
scripts
would like to use very similar information:move it to a central place instead (a file in
Mathlib/Util
). Suggestions for better locations are welcome!Also, split the
getAll
function in two pieces, getting the file names and transforming this into module names.While #11853 only requires the latter, #13245 needs the former (which is computed anyway).
Only accessible the converted module names and converting them back to files would be absurd.
lake exe mk_all
as a Lean executable #11853 which adds these utility functions