Hello; help with setup error (Win11, system_category 193)

Stream: new members

[Jan Grabowski]

Hello everyone, newbie here. Looking forward to getting into Lean. (I do have a real identity too: http://www.maths.lancs.ac.uk/~grabowsj/)

I am having issues getting set up with Lean4 via VS Code on Windows 11 (Windows user for... reasons of inter-operability with others, let's say). I think this probably isn't a Lean issue, but maybe others have encountered it and can help - Google isn't helping enough.

In a nutshell, I've followed the install instructions and downloaded the mathematics-in-lean project. When it tries to start, I get this error - I've highlighted what I think the root error is, namely a system_category error 193.

My guess is some sort of permissions problem, but any suggestions welcome.

c:\Users\Jan Grabowski\Documents\lean\mathematics-in-lean> lean --version
Lean (version 4.10.0-rc2, x86_64-w64-windows-gnu, commit 702c31b80712, Release)
c:\Users\Jan Grabowski\Documents\lean\mathematics-in-lean> lake --version
Lake version 5.0.0-702c31b (Lean version 4.10.0-rc2)
c:\Users\Jan Grabowski\Documents\lean\mathematics-in-lean> lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '.\.\.lake/packages\mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.\.lake/packages\Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.\.lake/packages\aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.\.lake/packages\proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '.\.\.lake/packages\importGraph'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '.\.\.lake/packages\Cli'
✔ [1/10] Fetched proofwidgets:optRelease
✖ [2/10] Building Cache.IO
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\Jan Grabowski\.elan\toolchains\leanprover--lean4---v4.10.0-rc2\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false .\.\.lake/packages\mathlib\.\.\Cache\IO.lean -R .\.\.lake/packages\mathlib\.\. -o .\.\.lake/packages\mathlib\.lake\build\lib\Cache\IO.olean -i .\.\.lake/packages\mathlib\.lake\build\lib\Cache\IO.ilean -c .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c --json
error: failed to execute 'c:\Users\Jan Grabowski\.elan\toolchains\leanprover--lean4---v4.10.0-rc2\bin\lean.exe': unspecified system_category error (error code: 193)
Some builds logged failures:

• Cache.IO
  error: build failed
  => Operation failed. Exit code: 1.

[Jan Grabowski]

PS. I get the same error manually running "lake exe cache get" in a Command Prompt or PowerShell, so VS Code appears not to be to blame.

[Jan Grabowski]

PPS. Turns out an alternative that works is to install Lean into an Ubuntu on Windows Subsystem for Linux :-)

Edit: and VS Code appears to be quite smart wrt WSL - since it had already logged me in to my Github account, I think it must be running the Windows version but connects to WSL to do stuff.

[Marc Huisinga]

Is there a file c:\Users\Jan (i.e. does the file Jan in c:\Users exist)?

[Jan Grabowski]

@Marc Huisinga there's just a space in my Windows username - other things succeeded in that directory structure so I don't think that's the issue.

[Marc Huisinga]

Still, does that file exist?

[Jan Grabowski]

Yes, it does.

[Marc Huisinga]

In that case, you can try deleting it.
This will be fixed in the next release candidate (fixed in lean4#4515 that releases in the next couple of days).

[Marc Huisinga]

I'm still not entirely sure which program creates these files, though! It's likely another program that does not deal with user names that contain spaces correctly.

[Jan Grabowski]

Ah. I see what's happening - thanks for linking to the other thread. Deleting the 5 random files has fixed the original problem. Now I can just decide whether to work in Win or Linux, I guess... Much appreciated, @Marc Huisinga and useful to know that there's a fix in progress.