Zulip Chat Archive

Stream: new members

Topic: Lean/vs codium crashing

Rémi Bottinelli (Oct 29 2022 at 16:26):

Hey, so for no apparent reason, either running leanproject build or launching codium on an (seemingly any) mathlib branch makes both crash, with no error message, and actually even the terminal from which I lanched the program closing too. This is with cache files present.
The memory consumption seems quite high, so this is maybe linux oom-ing the process… Any idea how to debug this?

Kevin Buzzard (Oct 29 2022 at 16:28):

What happens with lean --make src?

Kevin Buzzard (Oct 29 2022 at 16:29):

Are you sure your computer is not having serious problems like disc or memory failures?

Kevin Buzzard (Oct 29 2022 at 16:29):

Did you try rebooting?

Rémi Bottinelli (Oct 29 2022 at 16:30):

I tried rebooting. My computer is quite old indeed, but any other program seems fine. Let me test lean --make src.
(No crash as of ~7mn running time)

Rémi Bottinelli (Oct 29 2022 at 16:52):

While waiting: what would a crash/no crash for --make src mean?

Kevin Buzzard (Oct 29 2022 at 17:01):

There are tons of reasons that a program would crash

Kevin Buzzard (Oct 29 2022 at 17:02):

If you have no disc space, if you have no memory, if you have a faulty component or a corrupted operating system or if another program is out of control