error: unknown command '+leanprover-community/mathlib4:lean-

Stream: new members

[Jens Petersen]

Seems worth addressing this mathlib4 readme "bug": https://github.com/leanprover-community/mathlib4/issues/11031 ?

$ lake +leanprover-community/mathlib4:lean-toolchain new your_project_name math
error: unknown command '+leanprover-community/mathlib4:lean-toolchain'

[Jens Petersen]

Or is it better open a separate issue for https://github.com/leanprover-community/mathlib4/issues/11031#issuecomment-2008319725 ?

[Jens Petersen]

Perhaps it would be better to move this to #mathlib documentation say?

[Sebastian Ullrich]

How did you set up Lean? It seems you're not using elan, but you should

[Jens Petersen]

Ah thank you - you are right: my lean4 wasn't installed with elan, I built it myself (it is a package for Fedora). Mm, perhaps the error message could make this clearer?

Well if this works for 90%+ of users then I suppose it is not a big deal.