lake new, "no such file"

Stream: new members

[Drew Moore]

Hello - trying to get lake build to work on the "hello world" example generated by "lake new". I'm on windows. Getting an error "uncaught exception: no such file or directory (error code: 2)", and it's not giving the missing file.

My version of lean is Lean (version 4.0.0-nightly-2023-05-09, commit ad4b822734ad, Release), and my version of lake is Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-05-09)

[Drew Moore]

is there a way to run lake build in verbose mode to get more logs of what could be the issue?

[Mario Carneiro]

can you show the exact sequence of commands you used and the contents of the relevant files?

[Mario Carneiro]

this could be a bug in lake, clearly "no such file" without printing the file itself is not good

[Drew Moore]

I will try to do an exact repro in a new repo (sorry - I lost this thread - learning zulip as well!)

[Drew Moore]

ok I went to the parent directory and did the following:

mkdir hello3
cd hello3
lake init hello3
lake build

[Drew Moore]

[0/4] Building Hello3
[1/4] Compiling Hello3
[1/4] Building Main
error: > c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o .\build\ir\Hello3.o .\build\ir\Hello3.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe` exited with code 1
[2/4] Compiling Main
error: > c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o .\build\ir\Main.o .\build\ir\Main.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe` exited with code 1

[Mario Carneiro]

and lake --version says what?

[Drew Moore]

Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-05-09)

[Mario Carneiro]

is there a file called Main.lean or Hello3.lean?

[Drew Moore]

C:\Users\Nazerke\Documents\Drew\lean\hello3 [master +5 ~0 -0 !]> ls


    Directory: C:\Users\Nazerke\Documents\Drew\lean\hello3


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
d-----         5/12/2023   8:06 PM                build
-a----         5/12/2023   8:06 PM             24 .gitignore
-a----         5/12/2023   8:06 PM             20 Hello3.lean
-a----         5/12/2023   8:06 PM            222 lakefile.lean
-a----         5/12/2023   8:06 PM             36 lean-toolchain
-a----         5/12/2023   8:06 PM             74 Main.lean

[Drew Moore]

yes have both Main.lean and Hello3.lean

[Mario Carneiro]

can you find all the files mentioned in the error line? leanc.exe, Hello3.o and Hello3.c

[Drew Moore]

good call - there is no .\build\ir

[Drew Moore]

oh sorry
it's there

[Mario Carneiro]

can you run c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o .\build\ir\Hello3.o .\build\ir\Hello3.c -O3 -DNDEBUG directly?

[Drew Moore]

the object files are not in \build\ir

[Drew Moore]

ls build/ir


    Directory: C:\Users\Nazerke\Documents\Drew\lean\hello3\build\ir


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         5/12/2023   8:07 PM           1406 Hello3.c
-a----         5/12/2023   8:07 PM           3547 Main.c

[Mario Carneiro]

in my project it looks like build/ir has the .o and .c files and build/lib has .so, .ilean and .olean files (and a bunch of .trace files)

[Drew Moore]

.\build\ir\Hello3.o is missing

[Drew Moore]

should I try a different version of lake?

[Mario Carneiro]

actually I suppose that is to be expected since the leanc invocation was supposed to produce it

[Mario Carneiro]

what happens if you run leanc directly like I suggested?

[Drew Moore]

same error

[Drew Moore]

uncaught exception: no such file or directory (error code: 2)

[Mauricio Collares]

Does the command Mario suggested work if you replace the backslashes by forward slashes?

[Mauricio Collares]

(for the leanc arguments, I mean)

[Drew Moore]

just tried that, same error

[Drew Moore]

c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o
./build/ir/Hello3.o ./build/ir/Hello3.c -O3 -DNDEBUG
uncaught exception: no such file or directory (error code: 2)

[Mauricio Collares]

That's a very unhelpful error message. Yaël had the same thing, and they were running the commands inside VS Code's terminal (using bash). Where are you running this command?

[Drew Moore]

also vs code's terminal

[Drew Moore]

not sure what the default terminal is

[Drew Moore]

I'll try in powershell

[Drew Moore]

different (but worse?) behavior - now failing on Main compilation as well

C:\Users\Nazerke\Documents\Drew\lean\hello3 [master +5 ~0 -0 !]> lake build
[1/4] Compiling Hello3
[2/4] Compiling Main
error: > c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o .\build\ir\Main.o .\build\ir\Main.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe` exited with code 1
error: > c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe -c -o .\build\ir\Hello3.o .\build\ir\Hello3.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\Nazerke\.elan\toolchains\leanprover--lean4---nightly-2023-05-09\bin\leanc.exe` exited with code 1

[Drew Moore]

oh sorry that's the same as before

[Drew Moore]

fwiw, cmd has same behavior

[Mauricio Collares]

Yeah, I don't know :( Sorry for interrupting Mario's debugging session. It would be very good to have some leads on this, you're not the first user reporting this exact problem

[Drew Moore]

no thanks for chiming in!

[Mario Carneiro]

Unfortunately I also don't know, and I don't have a windows to test other things with

[Mauricio Collares]

This being Windows (and it being an issue which affects a random subset of users), I have to wonder: do you run some sort of antivirus software? I don't believe Windows Defender would be buggy, but almost every other AV does funny stuff

[Mario Carneiro]

oh, you could check the permissions on the Hello3.c file

[Mario Carneiro]

also, leanc is just a wrapper around a C compiler so it's possible you don't have the C compiler and that's what the error is about

[Drew Moore]

I'm also more comfortable in a unix environment haha

    Directory: C:\Users\Nazerke\Documents\Drew\lean\hello3\build\ir


Mode                 LastWriteTime         Length Name
----                 -------------         ------ ----
-a----         5/12/2023   8:07 PM           1406 Hello3.c
-a----         5/12/2023   8:07 PM           3547 Main.c

[Drew Moore]

that seems wrong

[Mario Carneiro]

even though lean ships with a C compiler, maybe an AV deleted it

[Mario Carneiro]

I don't know what -a---- means, but that's what all the files you have are reporting, so it seems okay?

[Drew Moore]

I see

[Drew Moore]

this will just be my excuse to get a unix personal laptop!

[Drew Moore]

thanks for the help. was hoping a Microsoft research product would work ok on windows, but even they're leaning linux these days :grinning:

[Drew Moore]

though could be user error for sure

[Mario Carneiro]

does it work on WSL?

[Drew Moore]

WSL?

[Mario Carneiro]

windows subsystem for linux

[Drew Moore]

ah have not set that up

[Mario Carneiro]

it's like a linux dev environment on windows

[Mario Carneiro]

if you have used msys2 it's kind of like that, only official MS

[Drew Moore]

yeah I'll finally bite the bullet and setup a linux partition for my laptop

[Drew Moore]

ty for the help - I've got to log off. hopefully will be back with more noob questions later!

[Mauricio Collares]

Mario Carneiro said:

also, leanc is just a wrapper around a C compiler so it's possible you don't have the C compiler and that's what the error is about

@Yaël Dillies Do you use some sort of antivirus software on your Windows machine? We just got a second bug report with the same symptoms you described for the lake exe cache get failure and we were wondering if the antivirus could be causing it.

[Mauricio Collares]

One could submit the C compiler binary shipped with Lean to virustotal to see if which (if any) antivirus software wrongly flags it as malicious

[Mario Carneiro]

aha: I found Leanc.lean in lean4 repo and it is indeed a simple lean file which calls a C compiler. If you do leanc.exe without arguments it prints the compiler it will call in the help message

[Mauricio Collares]

Also, is this Windows 10 or Windows 11? Maybe there is a difference. Windows has something called the "Attachment Manager" which automatically marks files downloaded from the internet as unsafe in some cases, and this might be "improved" in Windows 11.

[Yaël Dillies]

I think Windows Defender is on most of the time, and I also have Malwarebytes. Will try to disable both and see what happens. But I doubt it's related since my bug clearly is a Linux/Windows path syntax mismatch.

[Mauricio Collares]

Thanks for testing! You might have to reinstall the lean toolchain if it's an antivirus problem (elan uninstall whatever toolchain is being used by mathlib and then let elan download it again after the antivirus is off)

[Mauricio Collares]

I was referring to this other error log you posted (after the path normalization issue was fixed by Arthur), by the way: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20exe.20cache.20get/near/321148326

[Mauricio Collares]

Testing Mario's idea of calling leanc.exe directly to see what the wrapper will call would be very useful too