search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.49k stars 392 forks source link

Minimize `Lake` closure #2534

Open Kha opened 1 year ago

Kha commented 1 year ago

This was discussed at around https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/running.20.60cache.20get.60.20as.20part.20of.20every.20.60lake.20build.60/near/390475641. From a cursory glance, most Lean dependencies are only used in macro rules and elaborators, which could be moved out and made builtin_. Avoiding Lean.Parser/Elab should already provide a significant reduction of the closure and thus load time.

Kha commented 1 year ago

Ah, the output of mathlib's lake exe graph --to Lake --include-deps should also be helpful