Zulip Chat Archive

Stream: new members

Topic: lean assertion violation, cpp error


Peter Gumm (Jun 02 2022 at 16:16):

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 (Jun 02 2022 at 16:20):

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 (Jun 02 2022 at 16:20):

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

Peter Gumm (Jun 02 2022 at 16:23):

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

Julian Berman (Jun 02 2022 at 16:24):

Via elan you mean?

Peter Gumm (Jun 02 2022 at 16:26):

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

Julian Berman (Jun 02 2022 at 16:26):

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 (Jun 02 2022 at 16:26):

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 (Jun 02 2022 at 16:29):

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

Kevin Buzzard (Jun 02 2022 at 16:31):

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 (Jun 02 2022 at 16:31):

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

Kevin Buzzard (Jun 02 2022 at 16:33):

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 (Jun 02 2022 at 16:35):

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 (Jun 02 2022 at 16:36):

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

Kevin Buzzard (Jun 02 2022 at 16:37):

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

Peter Gumm (Jun 02 2022 at 16:42):

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 (Jun 02 2022 at 16:43):

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

Peter Gumm (Jun 02 2022 at 19:58):

:+1: Seems, I got everything working !


Last updated: Dec 20 2023 at 11:08 UTC