Lean setup

Stream: new members

[Vasily Ilin]

I followed the installation instructions for Windows and got no error but Lean infoview does not load. It just hangs in the state like below: image.png . What should I do to fix this?

[Alex J. Best]

I think we need more info to debug this, what project did you open, and how did you download it?

[Alex J. Best]

Maybe a screenshot of the whole of vscode would help at least

[Vasily Ilin]

@Alex J. Best , your question alone resolved the issue. It made me remember that I cannot just clone a Github repo but must do leanproject get instead. Thanks :)

[Peter Tupoiu]

Hello, I am experiencing errors after following the lean setup guide.

PS C:\Users\Peter Lastname\Documents\code\lean\sandbox\first_project> lake build
Ô£û [1/7] Building FirstProject.Basic
trace: .> LEAN_PATH=.\.\.lake\build\lib PATH c:\Users\Peter Lastname\.elan\toolchains\leanprover--lean4---stable\bin\lean.exe .\.\.\.\FirstProject\Basic.lean -R .\.\.\. -o .\.\.lake\build\lib\FirstProject\Basic.olean -i .\.\.lake\build\lib\FirstProject\Basic.ilean -c .\.\.lake\build\ir\FirstProject\Basic.c --json
error: failed to execute 'c:\Users\Peter Lastname\.elan\toolchains\leanprover--lean4---stable\bin\lean.exe': unspecified system_category error (error code: 193)
Some builds logged failures:
- FirstProject.Basic
error: build failed

[Peter Tupoiu]

My system information is this:

Operating system: Windows_NT (release: 10.0.22631)
CPU architecture: x64
CPU model: 16 x AMD Ryzen 7 4800H with Radeon Graphics
Available RAM: 16.50 GB

VS Code version: Reasonably up-to-date (version: 1.92.0)
Lean 4 extension version: 0.0.176
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.9.0)
Project: Valid Lean project (path: c:\Users\Peter Lastname\Documents\code\lean\sandbox\first_project)

---

Elan toolchains:

leanprover/lean4:stable (overridden by '\\?\C:\Users\Peter Lastname\Documents\code\lean\sandbox\first_project\lean-toolchain')

Lean (version 4.9.0, x86_64-w64-windows-gnu, commit 1b78cb4836cf, Release)

[Sebastian Ullrich]

Hi, some malfunctioning program probably created the file C:\Users\Peter, please remove it: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VS.20Code.20lean.20server.20crash/near/453296158

[Peter Tupoiu]

Sebastian Ullrich said:

Hi, some malfunctioning program probably created the file C:\Users\Peter, please remove it: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VS.20Code.20lean.20server.20crash/near/453296158

Hi Sebastian, I'm on a windows machine, and my user is called Peter Lastname (I am swapping out my last name to be more anonymous, to be clear). On windows it's possible to have folders with a space in.

(edit: ah, I have read the linked comment, let me double check!)

[Peter Tupoiu]

Aha, this seems to have worked! The file looks to have been created by the Wix website editor software I downloaded last september.

Do you think there's a way to prevent this bug from happening? Prioritising "C://x" in "C://x y/file.txt" seems wrong for quoted filepaths.

[Marc Huisinga]

Peter Tupoiu said:

Aha, this seems to have worked! The file looks to have been created by the Wix website editor software I downloaded last september.

Do you think there's a way to prevent this bug from happening? Prioritising "C://x" in "C://x y/file.txt" seems wrong for quoted filepaths.

This bug should be fixed as of v4.11.0-rc1. Upgrading from 4.9.0 to that version should also resolve that issue.

[Marc Huisinga]

(See also lean4#4515)