Zulip Chat Archive

Stream: lean4

Topic: Lean Assertion Violation

Mac (Jun 29 2022 at 05:24):

I am now frequently encountering the following error when the Lean server builds Lake modules:

LEAN ASSERTION VIOLATION
File: <home>\.elan\toolchains\leanprover--lean4---nightly-2022-06-17\include/lean/lean.h
Line: 570
offset >= lean_ctor_num_objs(o) * sizeof(void*)

Any ideas on what could trigger such an error? If not, and it bothers me enough, I will try to better nail down its cause.

Sebastian Ullrich (Jun 29 2022 at 05:27):

It sure doesn't look good. It should only happen in debug mode though, are you deliberately using that?

Good question. I did not think so, but upon further thought, due to my merging of linking and compiling with lake#89, I may have accidently enabled it as I do not pass the relevant C compiler arguments (e.g., -DNDEBUG) to the linking command. I guess it also means that the assertion violation is coming from Lake, not Lean.

Sebastian Ullrich (Jun 29 2022 at 07:06):

If you also elided -O3, that would very well explain any supposed compilation speedups :)

Mac (Jun 29 2022 at 07:38):

Sebastian Ullrich said:

If you also elided -O3, that would very well explain any supposed compilation speedups :)

Ahh.... yeah, that might explain it. :face_palm:

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib