-
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] - feat: lake exe mk_all
as a Lean executable
#11853
Conversation
6f992fa
to
d8635b9
Compare
mk_all
script implemented in Leanlake exe mkAll
as a Lean executable
@joneugster, do you think the same thing here as on #8361? |
Not necessarily. I personally care about import-analysis tools being outside of mathlib because I want to use them in my projects without importing mathlib. But generally, while having separate packages with useful utilities is nice for projects not depending on mathlib, with the current in-development state of lake, it's still quite tedious to keep all packages in sync and up to date... And finally, it's quite quick to extract useful stuff out of mathlib, once somebody concretely needs it. (The only reason I see to directly PR to a separate repo is that one can save some reviewer capacity if it's only utility-code) |
I also think that "import" requirements are quite project-specific. Even this tool is not just "import all files and/or all libraries":
It seems like one of these commands that are hard to implement in a way that pleases most projects. |
Thanks for the quick response! I'll trust Mario and Kim on |
🚀 Pull request has been placed on the maintainer queue by grunweg. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks plausible enough to me but I don't have any real Lean scripting experience so I'm hesitant to give definitive judgement.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the changes! I'm going to hold off on merging as I said, so let's kick this back on the maintainer queue:
maintainer merge
🚀 Pull request has been placed on the maintainer queue by Vierkantor. |
I've proposed moving the common code into |
bors merge |
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
Pull request successfully merged into master. Build succeeded: |
lake exe mk_all
as a Lean executablelake exe mk_all
as a Lean executable
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
… `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
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
… `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
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
… `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
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
… `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
Running
should have the same effect as running
that is, it creates the files
Mathlib.lean
,Mathlib/Tactic.lean
,Archive.lean
,Counterexamples.lean
.It does not create analogous files for
Cache
andLongestPole
.is similar, but uses all the
.lean
files inMathlib
, not just the Git-managed ones.See #11874 for using the script in CI.