search

leanprover / elan

The Lean version manager
Apache License 2.0
297 stars 34 forks source link

feat: support tar.zst archives #56

Closed gebner closed 2 years ago

gebner commented 2 years ago

As discussed on https://github.com/leanprover/lean4/pull/733, zstd produces significantly smaller binaries and is faster to decompress than gzip. So it would make sense to switch to tar.zst on linux.

This PR detects the archive format based on the file extension of the release file name (instead of the current linux=tar.gz, windows=zip logic). All archive formats are supported on all platforms. I believe this would even allow us to provide both zip and tar.zst releases on windows and elan would pick the tar.zst file first.

lean +gebner/lean:vzst --version (lean 3 commit, 10M -> 7M) (Lean 4 build is a bit more complicated because the cmake version in nixos-19.03 is too old to support zstd.)

Old elan version complain about "invalid gzip header" or "binary package was not provided for 'linux'" if the archive format is zst instead of gz.

Kha commented 2 years ago

Thanks!!

Lean 4 build is a bit more complicated because the cmake version in nixos-19.03 is too old to support zstd

This will be easy to solve in leanprover/lean4#733, we only need $GLIBC to be old now

gebner commented 2 years ago

Lean 4 build is alive as well: lean +gebner/lean4:vzst --version 113M -> 81M https://github.com/gebner/lean4/commit/32db7ae08a461e9f658fd068ec05643adfe5c1d7