8000 feat: make math Lake template follow Mathlib standards by Vierkantor · Pull Request #8866 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: make math Lake template follow Mathlib standards #8866

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 12 commits into from
Jun 23, 2025
Merged

feat: make math Lake template follow Mathlib standards #8866

merged 12 commits into from
Jun 23, 2025

Conversation

Vierkantor
Copy link
Contributor
@Vierkantor Vierkantor commented Jun 18, 2025 •
edited
Loading

This PR upgrades the math template for lake init and lake new to configures the new project to meet rigorous Mathlib maintenance standards. In comparison with the previous version (now available as lake new ... math-lax), this automatically provides:

  • Strict linting options matching Mathlib.
  • GitHub workflow for automatic upgrades to newer Lean and Mathlib releases.
  • Automatic release tagging for toolchain upgrades.
  • API documentation generated by doc-gen4 and hosted on github.io.
  • README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to math-lax.

@Vierkantor
feat: Lake template for "Mathlib-standard" projects
91025bf 
This PR adds a new `mathlib-dep` template to `lake init` and `lake new` which configures the new project to meet rigorous Mathlib maintenance standards. In comparison with the permissive `lake new ... math` template, this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by leanprover/doc-gen4 and hosted on `github.io`.

Potential areas for discussion:

* Template name. Maybe `mathlib-standard` instead, although this is less succinct?
* Should some of these features be added to the `math` template too? (Perhaps every one of these, in disabled form?)
@Vierkantor
Remove outdated TODO comments.
580e83c
@Vierkantor Vierkantor requested a review from tydeu as a code owner June 18, 2025 13:49
@tydeu
Copy link
Member
tydeu commented Jun 19, 2025 •
edited
Loading

Looks pretty good to me! I think this operating as a separate template is a great place to start. If everyone ends up using the new template or if there are some particular features that people really love and would like to see in the math template, then they can be further merged. Separately, I am not sold on the name. I think mathlib-dep doesn't do much to illustrate what makes it different from the less opinionated math template. Perhaps just mathlib is fine? I wish I had a good suggestion here.

The code seems generally reasonable. I will take a closer look once the CI passes. One thing I did notice was missing was a mention of the new template in the help text for new/init in Lake.Cli.Help. I would also suggest adding some tests the to test script in src/lake/tests/init that verify the package generation works as expected. (If you add tests and want CI to check it, you will need to temporarily enable the Lake tests on the PR by uncommenting this line.)

@Vierkantor
Copy link
Contributor Author
Vierkantor commented Jun 19, 2025 •
edited
Loading

Thanks for the review and helpful pointers!

For now, let's use mathlib as the template name.

I've added a test checking the linting options are set correctly. I also have a test repository on GitHub here: https://github.com/Vierkantor/lake-template-tester (it turns out that one of the workflows does not like force-pushes to the main branch)!

@Vierkantor
Always use mathlib's toolchain when initializing a new project.
9e28e92 
Previously, on dev builds Lake would complain that there was no known toolchain. But outside of dev builds we set this toolchain unconditionally to Mathlib's, so why not do it for dev builds too?
@Vierkantor
Copy link
Contributor Author

I pushed a change to the toolchain logic that should (hopefully) fix the tests. My reasoning is: outside of dev builds, we always select Mathlib's toolchain. So even if the current build is a dev build, we can still use that toolchain. Did I get this right?

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 19, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 19, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86eded35db40fadcd718eed738e0860b942841b1 --onto 0077dd3d5569527f023865099890fa5aa9ffbe77. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-19 17:31:47)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86eded35db40fadcd718eed738e0860b942841b1 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-23 13:07:10)

tydeu
tydeu approved these changes Jun 19, 2025
View reviewed changes
Copy link
Member
@tydeu tydeu left a comment

Choose a reason for hiding this comment

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

LGTM!

@Vierkantor @tydeu
Remove useless pattern match.
9f86042 
Co-authored-by: Mac Malone <tydeu@hatpress.net>
@kim-em
Copy link
Collaborator
kim-em commented Jun 20, 2025

I vote we be opinionated about this, and have this replace the math template, and renamed that to ... I don't know math-sloppy? Maybe math-scratch or math-lax?

@Vierkantor
Copy link
Contributor Author

Sounds good to me. I like math-lax, since the template itself is not being sloppy, the user is (allowed to be) :)

@Vierkantor
Rename mathlib -> math -> math-lax
5a3027d 
Change option naming so `lake new ... math` will add all the Mathlib-standard linting and CI workflows. The original `math` template is now called `math-lax`.
@Vierkantor Vierkantor changed the title feat: Lake template for "Mathlib-standard" projects feat: make math Lake template follow Mathlib standards Jun 23, 2025
Vierkantor
Vierkantor commented Jun 23, 2025
View reviewed changes
@Vierkantor
Copy link
Contributor Author

Kim approved the PR in our meeting today, so I'm going to go ahead and hit merge. Thanks for the reviews!

@Vierkantor Vierkantor enabled auto-merge June 23, 2025 13:17
@Vierkantor Vierkantor added this pull request to the merge queue Jun 23, 2025
Merged via the queue into master with commit ecf670e Jun 23, 2025
15 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 23, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
73237a6 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 23, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
2f7abda 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 23, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
daef64f 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 23, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
7900ed4 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 23, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
c1b6f3d 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@Vierkantor @tydeu @wkrozowski
feat: make math Lake template follow Mathlib standards (leanprover#8866)
0aba87d 
This PR upgrades the `math` template for `lake init` and `lake new` to
configures the new project to meet rigorous Mathlib maintenance
standards. In comparison with the previous version (now available as
`lake new ... math-lax`), this automatically provides:

* Strict linting options matching Mathlib.
* GitHub workflow for automatic upgrades to newer Lean and Mathlib
releases.
* Automatic release tagging for toolchain upgrades.
* API documentation generated by
[doc-gen4](https://github.com/leanprover/doc-gen4) and hosted on
`github.io`.
* README with some GitHub-specific instructions.

The previous edition of the template is still available, renamed to
`math-lax`.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tydeu tydeu tydeu approved these changes

Assignees
No one assigned
Labels
changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Vierkantor @tydeu @leanprover-community-bot @kim-em
0