Zulip Chat Archive

Stream: new members

Topic: Problems with LEAN

Sofia Salazar (Dec 27 2021 at 21:07):

Hi, How can I solve this problem?
tut.PNG

Adam Topaz (Dec 27 2021 at 21:16):

How did you install lean? Did you follow the official instruction from the community webpage?

Sofia Salazar (Dec 27 2021 at 21:22):

Yes, I did everything it says here
https://leanprover-community.github.io/install/windows.html

Adam Topaz (Dec 27 2021 at 21:24):

Are you opening a single lean file? It looks like you're inside a folder with c++ files

Sofia Salazar (Dec 27 2021 at 21:27):

Yes

Arthur Paulino (Dec 27 2021 at 21:31):

What shows up if you go to the TERMINAL tab of your console and type in lean -v?

Sofia Salazar (Dec 27 2021 at 21:55):

$ lean -v
← [31m ← [1merror: ← [0mcommand failed: 'lean.exe'
[1minfo: ← [0mcaused by: The file or directory is corrupted or unreadable. (os error 1392)

Matthew Ballard (Dec 27 2021 at 22:02):

A possible fallback approach is to

Install Lean in WSL

Install WSL and your preferred Linux distribution

For Windows 10, follow the instructions here.

For Windows 11, you can install through the Windows Store. This link will
open the WLS app page in the store. Next you will want to install the Virtual Machine Platform
component. Open up a Powershell with Administrator privileges by searching in the Windows omnisearch box
for Powershell and right clicking to select Administrator. Enter

dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all

Finally you can choose which Linux distribution exists. Continuing, we
will be assuming you choose Debian or Ubuntu.

Install Lean and Mathlib

Open up your WSL terminal and enter

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

If you in fact did not select Debian or Ubuntu see the installation instructions for other distributions.

Remove WSL VS Code, Install Windows VS Code and the extensions

The installation script for Mathlib also installed VS Code into WSL. Remove VS Code by entering

sudo apt remove code

into the WSL terminal.

Download and install VS Code for Windows. Next install the WSL Remote VS Code Extension and the Lean Extension.

Create a Lean project in WSL and open in Windows VS Code with code . .

Sofia Salazar (Dec 27 2021 at 22:05):

I think that somehow I already solve the problem, thanks a lot

Kevin Buzzard (Dec 27 2021 at 22:05):

At least one of your problems is caused by the fact that nowadays bare Lean 3 files which aren't in projects just don't work at all (I feel like once they used to, but now they don't). You _have_ to get a project and you _have_ to open the root directory of the project and then you can edit Lean files in that project.

Kevin Buzzard (Dec 27 2021 at 22:06):

If you just open a lean file nowadays then you get "Waiting for Lean server to start" in the infoview

Adam Topaz (Dec 27 2021 at 22:09):

I would try to make a new lean project and make a test.lean file there. As Kevin said, you should make sure to open the folder of the project, not an individual lean file.

Patrick Massot (Jan 08 2022 at 19:35):

I have one more user reporting that following the last instruction "Verify Lean is working, for example by saving a file test.lean and entering #eval 1+1. A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed." on https://leanprover-community.github.io/install/windows.html doesn't work at all.

Patrick Massot (Jan 08 2022 at 19:37):

So I removed that line.

Kevin Buzzard (Jan 08 2022 at 20:50):

I can believe this. We've had people on the chat recently who make the canonical mistake of opening a lean file not in a project and recently the error they get is of the form "lean is not running". I remember reproducing locally a few weeks ago

Last updated: Dec 20 2023 at 11:08 UTC