memory corruption

Stream: general

[Patrick Massot]

I just met a new error during a leanpkg build:

mathlib/src/group_theory/submonoid.lean: parsing at line 475
*** glibc detected *** lean: malloc(): memory corruption (fast): 0x00007fbcf5c4e18f ***
======= Backtrace: =========
[0xaa51b2]
[0xaa7ec5]
[0xaa93fd]
[0xa23d48]
[0x464a5e]
[0x464b89]
[0x4653f4]
[0x4656f3]
[0x47c038]
[0x47c317]
[0x731ca4]
[0x73206e]
[0xexternal command exited with status 139

and building stopped.

[Mario Carneiro]

is it reproducible?

[Mario Carneiro]

maybe it's cosmic rays :P

[Patrick Massot]

I relaunched leanpkg and it built successfully.

[Gabriel Ebner]

I had a similar problem when building mathlib using a debug build of Lean. Building mathlib failed due to assertions, which are disabled in the release build (used by elan). If these assertions are violated, you can very easily get memory corruption. (That is, these assertions check whether an array access is in bounds. And both reads and writes are out-of-bounds... I'm actually surprised this hasn't caused any bigger troubles yet.) This is the commit that replaces the out-of-bound array accesses by memory safe versions: https://github.com/leanprover-community/lean/pull/89/commits/7a94b7022b76e48bf2d9af0182932d30d99f1af8 It's part of https://github.com/leanprover-community/lean/pull/89 which is not merged yet.