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.

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

Use git lfs for stage0 to save space #1991

Open
Anderssorby opened this issue Dec 23, 2022 · 1 comment
Open

Use git lfs for stage0 to save space #1991

Anderssorby opened this issue Dec 23, 2022 · 1 comment

Comments

@Anderssorby
Copy link
Contributor

Suggestion

The lean4 repository takes up a large amount of space ~1.3GiB and that makes the experience less than ideal.
Since the stage0 is just generated and treated as binary data I suggest putting it into tracking by git-lfs to speed up downloads and reduce space needed. It tracks content hashes and registers and stores the data separately avoiding download of a large amount of data.
https://git-lfs.com/

git lfs track stage0

When downloading a fresh repo remember to git lfs checkout.

What do you think?

@Kha
Copy link
Member

Kha commented Jan 9, 2023

Some commments on LFS, mostly negative: https://news.ycombinator.com/item?id=27134972

to speed up downloads and reduce space needed

A far simpler solution for that would be to use a partial clone. git clone --filter=blob:none https://github.com/leanprover/lean4 uses 203MB of space, which is not significantly larger than a single checkout.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants