help setting up lean

Stream: lean4

[Aaron Liu]

I'm trying to work on lean4#7440. Since this is the first time I'm working on Lean, I forked the repository and cloned it. I then built lean with the instructions in the doc file at the lean4 repository here. I then followed the instructions in a different file here.

I've managed to get the directory in a configuration where lean --version throws an error, but I just finished multiple hours of building and would prefer to fix it rather than rip everything out and try again. Any help debugging this would be appreciated.

[Kim Morrison]

@Aaron Liu did you follow the instructions at https://lean-lang.org/lean4/doc/dev/index.html?

[Robin Arnez]

What error does lean --version throw, if I may ask?

[Robin Arnez]

Kim Morrison schrieb:

did you follow the instructions at https://lean-lang.org/lean4/doc/dev/index.html?

The second link Aaron provided is exactly the source file of that documentation.

[Robin Arnez]

A possible problem might be that you didn't properly copy the right .dll files. The command that's provided in the docs doesn't seem to do the trick sometimes, try:
ldd build\release\stage1\bin\lean.exe and copy the necessary files (under clang64 or something like that) into the same directory as the lean.exe.

[Aaron Liu]

Robin Arnez said:

What error does lean --version throw, if I may ask?

Errors(4)

Application popup: lean.exe - System Error : The code execution cannot proceed because libc++.dll was not found. Reinstalling the program may fix this problem.

Application popup: lean.exe - System Error : The code execution cannot proceed because libc++.dll was not found. Reinstalling the program may fix this problem.

Application popup: lean.exe - System Error : The code execution cannot proceed because libgmp-10.dll was not found. Reinstalling the program may fix this problem.

Application popup: lean.exe - System Error : The code execution cannot proceed because libuv-1.dll was not found. Reinstalling the program may fix this problem.

[Aaron Liu]

I fixed it (the answer was sfc /scannow or at least that's the last thing I did before it started working)

[Aaron Liu]

Now I have a different error (unknown module prefix Init, now Init.Prelude is the only file that works)

[Robin Arnez]

yeah I had that too

[Robin Arnez]

try: set LEAN_PATH=path\to\your\lean\thingy\build\release\stage1\lib\lean and then code . (or whereever your editor is)

[Robin Arnez]

That's some kind of issue of symlinks working differently with .. than on linux