lean assertion violation, cpp error

Stream: new members

[Peter Gumm]

Hi, I did install Lean under VS-Code on my Windows Computer. But after loading the tutorial and its first file "00_first_proofs.lean ", loading does not stop and I get a cpp error message:
LEAN ASSERTION VIOLATION
File: C:/projects/lean/src/frontends/lean/elaborator.cpp
Line: 3167
Task: c:\Users\gumm\tutorials\_target\deps\mathlib\src\logic\embedding.lean: equiv.subtype_injective_equiv_embedding
m_ctx.match(e, *val2)
LEAN ASSERTION VIOLATION
File: C:/projects/lean/src/frontends/lean/elaborator.cpp
Line: 3167
Task: c:\Users\gumm\tutorials\_target\deps\mathlib\src\order\hom\basic.lean: order_hom.dual
m_ctx.match(e, *val2)

[Kevin Buzzard]

Aah, that old assertion violation which was fixed years ago. Have you installed a very old version of Lean somehow? If you want to study the tutorial then you need to install it with leanproject and then open the root directory of the project folder with VS Code. Did you follow the instructions here to install Lean and leanproject?

[Julian Berman]

Can you confirm how you installed Lean? Did you follow this page?

[Peter Gumm]

Yes this is exactly what I did.
I installed lean via VS-Code.

[Julian Berman]

Via elan you mean?

[Peter Gumm]

I must admit I don't even know what elan does, yet I just blindly followed the instructions on that page.

[Julian Berman]

If you sit inside the tutorials directory in git bash, can you show us what lean --version says? (Let us know if you need more detailed instructions for doing that of course.)

[Julian Berman]

OK cool -- elan is basically a tool for installing lean versions. VSCode is a text editor, so a place where you can edit lean files.

[Peter Gumm]

$ lean --version
Lean (version 3.42.1, commit 68455b087d87, Release)

[Kevin Buzzard]

That looks good! The assertion violation is in Lean 3.4.2 (which looks a bit like 3.42 but is about 4 years older)

[Peter Gumm]

ok I am quite familiar with "Visual Studio" and with "VS-Code" (for Dafny, PVS, etc..)

[Kevin Buzzard]

I might be barking up the wrong tree, but I conjecture that the issue is that C:/projects/lean/src/frontends/lean/elaborator.cpp is not the Lean you want to use. That version of Lean looks suspiciously "globally installed" which is not what you want at all.

[Peter Gumm]

I recall that some time ago I already tried to install Lean - but gave up frustrated. So there might be old files lying around?

[Julian Berman]

Seems likely yeah -- can you show us what ls C:/projects/lean looks like from git bash?

[Kevin Buzzard]

If you go to VS Code settings and search for Lean, what does it say in Lean: Executable path?

[Peter Gumm]

Oh, yes, there is an old lean installation.
C:\\Users\\gumm\\lean-3.4.2-windows\\bin\\lean.exe
I'll remove that tonight and start the process anew.
Thanks A LOT for your help so far - need to tend my kid now ...

[Kevin Buzzard]

If you just change it to lean this might solve all your problems.

[Peter Gumm]

:+1: Seems, I got everything working !