Lean4 installation problems

Stream: new members

[Leandro Caniglia]

Even though I carefully installed VS Code (Windows) and followed the instructions for installing Lean4, I'm still unable to use it. Can someone figure out what I've done wrong? Thanks!

Some of the error messages I get:

1. Lean 4 server operating in restricted single file mode. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality.
2. 'Sandbox.lean' was closed in the meantime. Imports will not be rebuilt.
3. When trying #eval String.append("Hello, ", "Lean!") I get

Basic.lean:7:0
expression
  String.append
has type
  String → String → String
but instance
  Lean.Eval (String → String → String)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
Basic.lean:7:19
unexpected token '('; expected command

Clarification. I wrote the code in Basic.lean

[Mario Carneiro]

can you show a screenshot of the "explorer" view in vscode? What files exist and did you use "open folder" on the correct folder?

[Mario Carneiro]

the syntax #eval String.append("Hello, ", "Lean!") is incorrect, lean uses adjacency for function application so it should look like #eval String.append "Hello, " "Lean!" (or more conventionally #eval "Hello, " ++ "Lean!")

[Mario Carneiro]

Which instructions did you follow for installing lean4? (Could you link to it?)

[Leandro Caniglia]

image.png

I'm following Evaluating Expressions - Functional Programming in Lean (lean-lang.org)

[Leandro Caniglia]

The String.append issue is now clear. Thanks! Any idea of messages 1. and 2. above?

[Kevin Buzzard]

Have you created a valid Lean 4 project and tried using Lean on files within that project?

[Leandro Caniglia]

Yes. I clicked on the option to create a new Lean 4 project and that's why I now have the bunch of files shown in the screenshot.

[Kevin Buzzard]

The screenshot looks to me like things are working fine

[Tomas Uribe]

It appears you misread the manual : try #eval String.append "Hello, " "Lean!" instead. (The error message you posted is expected.)

[Leandro Caniglia]

Tomas Uribe said:

It appears you misread the manual : try #eval String.append "Hello, " "Lean!" instead.

Yes, you are right. Mario Carneiro already clarified it. Thanks!

[Timothy Chow]

I tried to install Lean 4 a few weeks ago on my Windows 10 laptop but something went wrong. VS Code seems to run fine and at first glance it seemed I had Lean 4 running, but I got an error message. Today I upgraded to Windows 11 and decided to revisit my installation of Lean 4. In VS Code when I click on "Install Lean" in the Lean 4 setup guide, I get the following error.

info: downloading installer to C:\Users\PC\AppData\Local\Temp\

error: could not create link from 'C:\Users\PC\.elan\bin\elan.exe' to 'C:\Users\PC\.elan\bin\lake.exe'

Elan failed with error code 1

=> Operation failed. Exit code: 1.

Any idea what I'm doing wrong? I'm prepared to uninstall everything and reinstall if that's the easiest approach, but I'm not even sure what I would need to uninstall to fix the problem.

[Timothy Chow]

I should also say that when I first opened up VS Code, after thinking for a while, it issued the following error message in the Lean InfoView.

c:\Users\PC\.elan\toolchains\leanprover--lean4---v4.24.0-rc1\bin\lake.exe setup-file C:/Users/PC/Documents/Lean_test2/LeanTest2/Basic.lean - failed:

stderr:
✖ [3/4] Running Mathlib.Data.Real
error: no such file or directory (error code: 2)
file: C:\Users\PC\Documents\Lean_test2\.lake\packages\mathlib\Mathlib\Data\Real.lean
✖ [4/4] Running setup-file C:/Users/PC/Documents/Lean_test2/LeanTest2/Basic.lean
trace: file identified as module: LeanTest2.Basic
error: LeanTest2\Basic.lean: bad import 'Mathlib.Data.Real'
Some required targets logged failures:

• Mathlib.Data.Real
• setup-file C:/Users/PC/Documents/Lean_test2/LeanTest2/Basic.lean
  error: build failed

[Timothy Chow]

I remember that when I first tried installing Lean, I messed around for a while, trying to create test files, possibly making things worse. Unfortunately, I don't remember any more exactly what I did back then.

[Kevin Buzzard]

That latter error could be completely consistent with your setup -- do you have a file called Basic.lean with the incorrect line import Mathlib.Data.Real which tries to import a file which doesn't exist?

[Timothy Chow]

Ah, yes! Here's a screenshot, which I just figured out how to post.
lean.png

If I replace the offending line then it seems to work. Thank you!

[Timothy Chow]

From the screenshot, can you spot anything else that I might have done wrong and that might cause me trouble down the line?

[Kevin Buzzard]

This is some Windows OS presumably? Those files exist for me in $HOME/.elan/bin, are they there for you? Can you write to them? If this is Windows then you might want to try turning off your firewall temporarily to see if it makes a difference.

[Timothy Chow]

Yes, this is Windows 11. I think that $HOME for me is C:\Users\PC because in there I see .elan and .vscode as well as Documents\mathematics_in_lean and Documents\Lean_test and Documents\Lean_test2 (which I now vaguely recall creating while I was troubleshooting). Inside .elan there is indeed a bin subdirectory containing elan.exe, lake.exe, lean.exe, leanc.exe, leanchecker.exe, leanmake.exe, leanpkg.exe. In particular, C:\Users\PC\.elan\bin\elan.exe and C:\Users\PC\.elan\bin\lake.exe both exist, and I can create new files in the bin directory without a problem. So I don't understand the "could not create link" error.

However, maybe it doesn't matter (for now) since I'm able to mess around in my Basic.lean file and do some examples, which is all I'm trying to do at this stage. Still, it might be nice to know what I did to mess things up.

[Bryan Gin-ge Chen]

Is the filesystem on your drive ExFAT by any chance? Just guessing from the error message you posted, but it might be related to this rustup issue (elan started as a fork of rustup).

[Marc Huisinga]

Bryan Gin-ge Chen said:

Is the filesystem on your drive ExFAT by any chance? Just guessing from the error message you posted, but it might be related to this rustup issue (elan started as a fork of rustup).

I haven't tried, but this error might also be caused by trying to re-install Elan while some instance of Lean is already running. I'll see if we can shut down the language server before trying to re-install Elan.

[Marc Huisinga]

I've confirmed that this exact error occurs when trying to re-install Elan on a Windows machine while a Lean server is already running.
Fix at vscode-lean4#678.

[Timothy Chow]

The filesystem on my drive is NTFS. But it sounds like the problem has been diagnosed. Is there anything I need to do? I seem to already have elan.exe so maybe I shouldn't have been trying to re-install it anyway, for no reason?

[Kevin Buzzard]

You might want to try an elan self update just to check that you have the latest version

[Timothy Chow]

"elan self update" triggers the "could not create link" error again.

[Kevin Buzzard]

Even after a reboot?

[Timothy Chow]

Okay, it's working now! I decided to just reinstall everything from scratch. I have a theory as to one thing I might have done wrong the first time. During the setup phase, a checklist appears, where I think the second item is "Books and documentation" or something, and the third item is "Install Lean" with a blue "Install" button. I clicked on "Install" and it worked, but then instead of automatically moving me to the next item in the checklist, it stayed on "Install Lean" and the blue "Install" button looked the same as before. So I assumed that something had gone wrong and I clicked "Install" again, which I don't think I was supposed to do. I don't know if this was the only thing I did wrong (or even if this was the cause of my problems), but I thought I would mention it.

[Divyansh Arora]

I am trying to install Lean4 on my laptop (Windows 11) from the follwoing link https://lean-lang.org/install/, and I am facing the following error:
PastedText.txt

From what is written in the end:
Some required builds logged failures:

• Mathlib.Data.FunLike.Basic
• Mathlib.Data.Quot
• Mathlib.Logic.Nontrivial.Basic
• Mathlib.Algebra.Group.Pi.Basic
• Mathlib.Algebra.Group.Nat.Units
• Mathlib.Algebra.GroupWithZero.Basic
• Mathlib.Data.List.Basic
  error: build failed

but there is no mention of what I can possibly do to prevent the build from failing.
In the start I had followed the legacy instructions, so I might have messed up there.

Should I delete everything and reinstall, or is there any possibility for fixing this? And if I should delete everything please do give an outline of the process because I have no Idea where/how to delete.

[Kevin Buzzard]

Where are you seeing this error? I mean, how are you running lean?

[Divyansh Arora]

I am running lean in VSCode. I am able to view the error in the Lean InfoView in VSCode.
Also I first get the error:
Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.

Then on restarting the file I get the above mentioned error

[Sham S]

I used to get this i reinstalled lean through vscode, even if you get it then run lake exe cache get and lake build through command line/PS. This works even if the restart file button won't work or fail due to various issues.

[Sham S]

https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

[Kevin Buzzard]

Can you send us a screenshot of VS Code showing the error in the infoview and also with the file explorer open? Here's what I'm working on right now as an example:
Screenshot from 2025-12-17 09-41-26.png

[Divyansh Arora]

Hi, Sham's first command has solved the issue, thanks a lot for the help @Kevin Buzzard and @Sham S !