On a more serious note, I tried to go exactly through the "Create a Lean Project" section here https://leanprover-community.github.io/install/project.html#creating-a-lean-project but after running `lake +v4.24.0 new my_project math` and downloading a bunch of stuff it fails with
```
[jdw@fedorabook lean]$ lake +v4.24.0 new my_project math
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:5: Invalid field `baseName`: The environment does not contain `Lake.Package.baseName`
rootPkg
has type
Package
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:24: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
pkg
has type
NPackage _package.name
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:173:34: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
toolchainContent
has type
String
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:194:16: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
pkg
has type
NPackage _package.name
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:175:13: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
toolchainContent
has type
String
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:177:29: Invalid field notation: Type of
toolchainVersion
is not known; cannot resolve field `dropPrefix`
error: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean: package configuration has errors
```
Anybody got an idea what I'm doing wrong?
Jakob
npub1at…90vsp
2026-01-17 07:31:14 UTC
in reply to nevent1q…sft7
Author Public Key
npub1at4g3kglwemnmyl7puvfkh6lvtukglp0wtvj0ql6uy67wuuwdjusn90vspSeen on
wss://relay.ditto.pubPublished at
2026-01-17 07:31:14 UTCEvent JSON
{
"id": "f9fef02cc98c5b986055dfda3ae970eb09bcc76dcf9aa731fa03bfe50a71970d",
"pubkey": "eaea88d91f76773d93fe0f189b5f5f62f9647c2f72d92783fae135e7738e6cb9",
"created_at": 1768635074,
"kind": 1,
"tags": [
[
"e",
"71b739e62c26b9c074a1abede2058ac2d82f3d4036cc8554e6e08d88ffff5057",
"wss://relay.ditto.pub",
"reply"
],
[
"content-warning",
"Error messages"
],
[
"proxy",
"https://mathstodon.xyz/users/jdw/statuses/115909268218957038",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "On a more serious note, I tried to go exactly through the \"Create a Lean Project\" section here https://leanprover-community.github.io/install/project.html#creating-a-lean-project but after running `lake +v4.24.0 new my_project math` and downloading a bunch of stuff it fails with\n```\n[jdw@fedorabook lean]$ lake +v4.24.0 new my_project math\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:5: Invalid field `baseName`: The environment does not contain `Lake.Package.baseName`\n rootPkg\nhas type\n Package\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:167:24: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`\n pkg\nhas type\n NPackage _package.name\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:173:34: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`\n toolchainContent\nhas type\n String\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:194:16: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`\n pkg\nhas type\n NPackage _package.name\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:175:13: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`\n toolchainContent\nhas type\n String\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean:177:29: Invalid field notation: Type of\n toolchainVersion\nis not known; cannot resolve field `dropPrefix`\nerror: /home/jdw/Projects/lean/my_project/.lake/packages/mathlib/lakefile.lean: package configuration has errors\n```\n\nAnybody got an idea what I'm doing wrong?",
"sig": "28982e0cf47f4c87a74a09e5d0f7a77d1651c4e0f872066b3a430e8da371fb63c5968b66d09c41dbc42628bf5332df5f0e2036bf8f0c8abd985c547cf5a970f3"
}