Zulip Chat Archive

Stream: lean4

Topic: Errors after bumping

Patrick Massot (Apr 28 2023 at 09:24):

(deleted)

Patrick Massot (Apr 28 2023 at 09:27):

Forget about the above message. It seems my hard drive is full, which a good reason to make a lot of things fail.

Patrick Massot (Apr 28 2023 at 09:31):

I just removed about twenty Lean 4 toolchains from my elan folder, so I'm good to go again.

Shreyas Srinivas (Apr 28 2023 at 13:45):

Patrick Massot said:

I just removed about twenty Lean 4 toolchains from my elan folder, so I'm good to go again.

The lake-packages folder for each math project created is 2GB. That is also quite a lot of space consumed

Patrick Massot (Apr 28 2023 at 13:47):

Thanks. I'm well aware of this issue.

Last updated: Dec 20 2023 at 11:08 UTC