Post #2994407
2026-05-27 01:43 UTC
I followed the instructions from https://lean-lang.org/install/ to install lean via VSCode and create a first project with mathlib, and then I ran
$ du -hs first-project/
7.0G first-project
SEVEN GIGABYTES
what the fuck is going on here? who the fuck thought this was an acceptable outcome?
Replies (4)
-
@rntz@recurse.social 2026-05-27 01:53
checking out a tutorial project and I need to "trust" the project folder - which AFAICT allows arbitrary code exec on my machine by whoever authored the repo - in order to interact with Lean code in any way, even syntax highlighting, it seems? What the actual fuck? Who thought the correct options were (a) things just don't work at all, (b) arbitrary code exec, and NOTHING IN BETWEEN? modern development baffles me.
-
@nemo@camp.crates.im 2026-05-27 03:31
@rntz@recurse.social lean is very lean man
-
@interpipes@thx.gg 2026-05-28 00:31
@rntz@recurse.social storage vendors
-
@gregsbrain@mstdn.social 2026-05-28 01:18
@rntz@recurse.social 7Gbytes of something something maintainable 🤔