RFC: size on disk for teaching

Proposal

This is somehow a meta-RFC that aims to track some general issue that probably involves several different technical questions. It is created in the context of providing the FRO with high priority issues. The general issue is the size of Lean and its libraries on disk.

This is especially relevant in teaching contexts. Two situations are common when teaching:

• Students have personal computers with limited space.
• Students use shared computers provided by their university with disk quotas.

In the second situation, one can sometimes work around the issue by using a shared copy of Mathlib, but this requires admin access for teachers. Teachers don’t have direct admin access and the official procedure to install things can take several months.

When using Lean 3, my students were able to follow my course with a Lean+mathlib folder weighting about 120Mb, and a copy of VSCode weighting 410Mb. Currently I have no idea how I will handle this in Lean 4. The naive idea of getting a Lean toolchain and a copy of Mathlib with olean files costs more than 5Gb (1 Gb for the Lean toolchain and 4Gb for Mathlib).

I don’t expect a single action to solve the issue. Some components may be:

• Tools allowing to prune dependencies. Maybe this is partly a documentation issue and lake can already help with that. Basically I would like to easily say my teaching library only depends on a subset of Mathlib so that only this subset would take up space on disk for students.
• Options allowing to store less information into olean files, as described in #2328
• Allowing to keep compressed oleans on disk, uncompressing them during import.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by separating the proposal's dependency-pruning, reduced-olean, and compressed-olean questions, then read the Lake-related context and issue #2328. A contribution would need a specific component and measurable disk-size goal, since this RFC does not define a single completion criterion.