Post #4119649

Likewise, mathlib being 7G compiled is not *that* ridiculous given it's a formalisation of substantial parts of modern math (as someone pointed out to me on twitter). And, yeah, many modern languages do per-project dependency management to avoid versioning difficulties. there is like, no individual part of this that is indefensible. but the combination of everything just results in something that is... not great as a first experience.