Lean4プロジェクトのリポジトリをローカルに持ってきてコードを見ようとすると大抵Mathlib4に依存している部分の膨大な定理のビルドが走って大変時間がかかるがあれをNixとかで一旦ビルドしたものをキャッシュしてどうにかしてくれないのかというところに普及の鍵がある気もする