feat: Switch from "math" to "mathlib" in the lake new <project> <template> syntax

[euprunin]

This PR switches the default template name from "math" to "mathlib" in the lake new <project> <template> command, while continuing to support "math" for backward compatibility. This clarifies the intended use and avoids ambiguity in naming.

[digama0]

👍 from me, this is the only place where "math" is used to refer to mathlib, nothing in mathlib's own documentation does this. (Also somehow every time I read this command I am reminded of New Math...)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-05-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 21:56:27)
• ✅ Mathlib branch lean-pr-testing-8487 has successfully built against this PR. (2025-05-27 19:22:49) View Log

[euprunin]

I'm getting: Error: feat/fix PR must have a changelog-* label.

Could someone help me add the appropriate changelog-* label? It looks like I don't have permission to add it myself.

[nomeata]

You can set that label with a comment with just the name of the label as the comment text.

[euprunin]

changelog-lake

[euprunin]

Is there anything I should improve in the implementation, or does the code look good as it is?

[tydeu]

Sorry for not replying here sooner! I appreciate the effort, but I am not sold on this change.

The math template is meant to be a standard template for a mathematics project in Lean. It is not merely a template which includes Mathlib. For example, the template may evolve to include additional dependencies or other configuration that would be helpful to end user math projects.

Separately, naming the template mathlib has its own potential for confusion. After all, there are different types of Mathlib projects, including forks of Mathlib and downstream math projects that merely depend on it. As the target of this template is the later, it makes sense to distinguish it a bit (which the more generic name of math is meant to do).

[euprunin]

@tydeu

The math template is meant to be a standard template for a mathematics project in Lean. It is not merely a template which includes Mathlib. For example, the template may evolve to include additional dependencies or other configuration that would be helpful to end user math projects.

Assuming that the math template is intended to serve as a standard template for mathematics projects in Lean, and not merely as a minimal template that includes Mathlib, then it seems that several pieces of documentation would need to be updated to reflect this broader purpose.

For example, the current lake new --help output states:

% lake new --help
…
The initial configuration and starter files are based on the template:
…
  math                  library only with a mathlib dependency

Personally, I would find it quite unintuitive if invoking lake new <project> math produced a project that included anything beyond Mathlib, given the current messaging ("library only with a mathlib dependency").

To date, I don't recall seeing any documentation, or even informal discussion (e.g., on Zulip), suggesting that the math template is intended to provide anything more than a Mathlib-based starter project.

[tydeu]

@euprunin Your intuition makes sense. There has not really been a need to distinguish these notions before as they are currently synonymous. This PR is the first real reason to express this intent.

Personally, I would find it quite unintuitive if invoking lake new <project> math produced a project that included anything beyond Mathlib, given the current messaging ("library only with a mathlib dependency").

Yes, this line would be updated if more was added. This documentation states what is currently generated, it can change if things change. That is, it is not indicative of what the math (or std) template might do in the future.

It may also be worth noting that there is some possibility in the future of there being another template that is more closely tied to Mathlib (e.g., with the same style options), which might better use the mathlib name.