Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Minimize Lake closure #2534

Closed
Kha opened this issue Sep 13, 2023 · 2 comments
Closed

Minimize Lake closure #2534

Kha opened this issue Sep 13, 2023 · 2 comments
Labels
Lake Lake related issue performance A performance problem related issue or PR

Comments

@Kha
Copy link
Member

Kha commented Sep 13, 2023 •
edited
Loading

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 Kha added Lake Lake related issue performance A performance problem related issue or PR labels Sep 13, 2023
@Kha
Copy link
Member Author

Kha commented Sep 13, 2023

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

@Kha
Copy link
Member Author

Kha commented Jan 14, 2025

Closing this given caching and TOML features added since

@Kha Kha closed this as completed Jan 14, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Lake Lake related issue performance A performance problem related issue or PR
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Kha