RFC: Provide a leanpkg binary to help confused new users

[eric-wieser]

Proposal

A lean4 toolchain should come with a leanpkg binary that informs the user that they are confused.

It should fail with an error, and print some combination of:

• A reminder that the leanpkg is for Lean 3, and they are (and should be!) using Lean 4
• Instructions to use lake instead
• A link to up-to-date documentation online
• A request to report any documentation that still mentions leanpkg on Zulip.

Community Feedback

This question comes up repeatedly on Zulip:

• no leanpkg in lean4/stable?
• no leanpkg.exe
• How to install leanpkg
• error: toolchain 'leanprover/lean4:v4.3.0' does not have the binary leanpkg

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

AFAIK that hasn't come up again in a long time so can probably be closed?