Zulip Chat Archive

Stream: new members

Topic: Problem installing lean 3 in WSL with leanpkg


Jim Portegies (Jan 16 2024 at 15:24):

Sorry if this is a duplicate question but I could not find the answer.

I am trying to start a new lean 3 project in which I want to import an existing lean 3 project. I have installed lean 3 in WSL (Windows Subsystem for Linux) according to the instructions here: https://leanprover-community.github.io/lean3/install/debian.html

Next I try to create a new project according to the instructions here https://leanprover-community.github.io/lean3/install/project.html#creating-a-lean-project, i.e. I write leanproject new my_project and I get the error:
toolchain 'stable' does not have the binary '.../leanpkg'

Does anyone know how to fix this?

Perhaps relevant, maybe not: I have lean 4 installed on the Windows side of my system

Thanks for any insights!

Mario Carneiro (Jan 16 2024 at 15:30):

Unfortunately leanproject is not accepting bugfixes anymore, so one has to work around this issue (which is caused by the fact that leanproject tries to get the latest version of lean but that's lean 4 now and it can't find leanpkg which is the lean 3 build tool). The workaround is to do:

elan override set leanprover-community/lean:3.51.1
leanproject new my_project
elan override unset
cd my_project
leanproject build

Jim Portegies (Jan 16 2024 at 15:43):

That worked! Thank you!


Last updated: May 02 2025 at 03:31 UTC