## Stream: general

### Topic: excessive memory

#### 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)


#### Kenny Lau (Sep 24 2018 at 16:06):

maybe you should increase memory consumption threshold

#### 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.

#### Johan Commelin (Sep 24 2018 at 16:06):

This is on an almost empty file

#### Johan Commelin (Sep 24 2018 at 16:07):

I just killed all Lean and VScodes

#### Johan Commelin (Sep 24 2018 at 16:07):

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

#### 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.

#### 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.

#### Johan Commelin (Sep 24 2018 at 16:11):

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

#### Reid Barton (Sep 24 2018 at 16:13):

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

#### Reid Barton (Sep 24 2018 at 16:13):

I guess probably not if your laptop is 11 years old

#### Johan Commelin (Sep 24 2018 at 16:14):

I have two single thread cpu's I think

#### Johan Commelin (Sep 24 2018 at 16:14):

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

Ah, okay

#### 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".

#### Reid Barton (Sep 24 2018 at 16:16):

I see this error a lot and just restart lean

#### Johan Commelin (Sep 24 2018 at 16:16):

But it is annoying when you get it right at startup

#### Johan Commelin (Sep 24 2018 at 16:17):

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

#### 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"

#### 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.

#### 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!)

#### 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)

#### Scott Morrison (Sep 25 2018 at 07:36):

I think for now anyone can create an account there.

#### Scott Morrison (Sep 25 2018 at 07:36):

It's running on quite fast hardware.

#### 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...

#### Scott Morrison (Sep 25 2018 at 07:37):

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

#### 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.

#### 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.

#### Reid Barton (Sep 25 2018 at 11:34):

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

#### Patrick Massot (Sep 25 2018 at 11:49):

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

#### 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.

#### 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.

#### 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

#### 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.

#### 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