Adam Bliss

Hm, it just occurred to me that perhaps I was supposed to solve this with a "kindbind" statement somewhere, but I've never understood exactly how to use them.

No, I never used the original gateway. My impression is that they retired it precisely because they wanted to add concepts like this that didn't fit naturally into the irc...

Here's a zipfile containing the core dump. [core.zip](https://github.com/leanprover/lean/files/1083290/core.zip) ``` #0 0x00bc8b10 in lean::scanner::next (this=0xbebcae80) at /home/abliss/proj/lean/src/frontends/lean/scanner.cpp:99 99 m_curr = m_curr_line[m_spos]; [Current thread is 1 (Thread 0xb6f4d000 (LWP 19129))] (gd (gdb)...

Anyway, it seems like the least invasive fix for this is to add `-fsigned-char` to the CXX_FLAGS in `CMakeLists.txt`. But I would suggest also enabling at least `-Werror=type-limits` . And...

Thanks @leodemoura , I'll give that a try and report back. Meanwhile, adding `-fsigned-char` allowed the build to progress (even with `-Werror`), but it eventualy failed again like this: ```...

Yeah, I figured that the `-fsigned-char` should've fixed it too, but it seems that the serializer code is unable to re-read the `coe.olean` file that it wrote. I'm stepping through...

BTW is there documentation on the `.olean` format somewhere? I'm not sure whether it's writing the .oleans badly or just reading them badly. The `.olean` files generated on ARM don't...

I tried reducing the library to just `init/core.lean`. If I run `lean --make`, it seems to _occasionally_ produce a valid core.olean. But most of the time it is corrupt. Is...

Thanks for those details. I can confirm that the bug still happens for me with `-j 0`, and it happens in exactly the same place as you: `psigma.sizeof` (`core.olean` line...

Amazing. I get the exact same result on my device (999877 with -fsigned-char, 1000000 without). Nice detective work. Sorry for suggesting `-fsigned-char` in the first place. I had originally worried...