Zulip Chat Archive

Stream: general

Topic: excessive memory


view this post on Zulip Johan Commelin (Sep 24 2018 at 16:06):

On my laptop I get the following error pretty often:

excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

view this post on Zulip Kenny Lau (Sep 24 2018 at 16:06):

maybe you should increase memory consumption threshold

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:06):

I also see in top that there are 8 processes of VScode open, whereas I just kill -9ed all of them.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:06):

This is on an almost empty file

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:07):

I just killed all Lean and VScodes

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:07):

Does this just mean that my laptop is too old for Lean?

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:09):

Hmm.. if I close the VScode window, all the processes are gone in top. I don't know why VScode spawns so many subprocesses if I have only one file open.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:11):

I have at least 2.5 GB of unused RAM on this box. I wish that would be enough.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:11):

Maybe I should try a reinstall of VScode. But this feels like cargo-cult troubleshooting.

view this post on Zulip Reid Barton (Sep 24 2018 at 16:13):

Were they really different processes? Do you have 8 cpus?

view this post on Zulip Reid Barton (Sep 24 2018 at 16:13):

I guess probably not if your laptop is 11 years old

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:14):

I have two single thread cpu's I think

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:14):

One socket with 2 cores; and 1 thread per core.

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:15):

They had different process id's

view this post on Zulip Reid Barton (Sep 24 2018 at 16:15):

Ah, okay

view this post on Zulip Reid Barton (Sep 24 2018 at 16:16):

I think "excessive memory" means Lean hit a limit it set for itself, though. Not "the machine is out of memory".

view this post on Zulip Reid Barton (Sep 24 2018 at 16:16):

I see this error a lot and just restart lean

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:16):

But it is annoying when you get it right at startup

view this post on Zulip Johan Commelin (Sep 24 2018 at 16:17):

If I'dd get it once a day I could live with it.

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 07:17):

It's a shame. So many people here, serious people, talk about issues with compile times and stuff like this. I use Lean on a 2-year-old PC with 8 cores and 16 gigs of ram, and mathlib compiles in 6 minutes. I think we need to crowd fund for better hardware for the community. I should edit the mathoverflow post -- "instead of upvoting, consider a $5 donation to the Lean Hardware Hardship fund"

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:35):

On the subject of hardware, I managed to install a version of CoCalc inside Docker yesterday, running on my hardware.

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:35):

It's at <https://54.91.0.213:8080/app> for now (no promises about uptime yet!)

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:36):

(and apologies that it is over https but there's no certificate; you may have to click through a warning, depending on your browser)

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:36):

I think for now anyone can create an account there.

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:36):

It's running on quite fast hardware.

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:37):

Unfortunately cocalc by default seems to kill long-running processes, so I can't actually run leanpkg build on mathlib to time it...

view this post on Zulip Scott Morrison (Sep 25 2018 at 07:37):

Hopefully there is a setting somewhere to disable this, but I haven't found it.

view this post on Zulip Kevin Buzzard (Sep 25 2018 at 08:00):

You might have to pay. I will learn more about this today (cocalc admin is on my list). I think the idea is that I get some credits for a project, and one of the things I can spend credits on is leaving processes to run for longer.

view this post on Zulip Reid Barton (Sep 25 2018 at 11:33):

@Scott Morrison, in case you're unfamiliar with it, https://certbot.eff.org/ is a very easy way to set up a properly-signed SSL certificate, at least on Ubuntu systems or similar.

view this post on Zulip Reid Barton (Sep 25 2018 at 11:34):

Though if you have some strange firewall setup, it might be a bit more complicated.

view this post on Zulip Patrick Massot (Sep 25 2018 at 11:49):

I created an account and tried to use Lean but it doesn't seem to work.

view this post on Zulip William Stein (Sep 26 2018 at 16:12):

Unfortunately cocalc by default seems to kill long-running processes, so I can't actually run leanpkg build on mathlib to time it...

Send me a link to your project (or open a support request by clicking Help with your project open in cocalc) and I'll increase the "idle timeout" from the default (30 minutes) to something much longer.

view this post on Zulip William Stein (Sep 26 2018 at 16:12):

You might have to pay. I will learn more about this today (cocalc admin is on my list). I think the idea is that I get some credits for a project, and one of the things I can spend credits on is leaving processes to run for longer.

Yep, that's the "idle timeout" quota.

view this post on Zulip Reid Barton (Sep 26 2018 at 17:47):

But Scott is running the CoCalc software on his own server, right? So Scott needs to make that idle timeout change in his own copy

view this post on Zulip Scott Morrison (Sep 26 2018 at 21:42):

Yes, @William Stein, this was a question about cocalc in Docker.

(Don't worry, I'm not being distracted by Docker; I'm working on getting courses signed up to the real cocalc too. :-)

At least in docker, the processes are being killed (exit code 137) much faster than every 30 minutes; it's more like 3 minutes.

view this post on Zulip William Stein (Sep 26 2018 at 22:25):

At least in docker, the processes are being killed (exit code 137) much faster than every 30 minutes; it's more like 3 minutes.

OK, that's weird. By default, I don't think anything is ever killed by cocalc in Docker, since there are no quotas/upgrades/etc. for docker-cocalc. Also, CoCalc doesn't kill processes when something is idle -- it kills entire projects. So it may be something particular to your Docker setup. What's the simplest example that I can try to reproduce of what you're observing?


Last updated: May 13 2021 at 22:15 UTC