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