Skip to content

Commit d574737

Browse files
committed
chore: bump leantar 0.1.8 (#8506)
The latest version of leantar [includes](digama0/leangz@v0.1.7...v0.1.8) the following features and bug fixes: * Compression for `.hash` files * Support for non-GMP bignum (de)compression This is a backward compatible release, meaning that v0.1.8 can understand .ltar files produced by v0.1.7 and previous versions. So there should not be any hiccups during the transition period. The important fix is the non-GMP bignum bug: previously, leantar would always compress and decompress olean files as if they contained GMP bignums, but GMP is only enabled on some architectures. The CI machines enable GMP, so compression is not a problem, but decompression happens on user machines of all architectures and this can cause crashes or invalid .olean files on MacOS Arm64, Linux Arm64 and Windows. Surprisingly, no one has noticed this, and I believe the reason is because mathlib has never contained a numeric literal of size 2^64 or larger. Lean [has one](https://github.com/leanprover/lean4/blob/65d08fdcdd9fb825b588660cce4e082a758954fa/src/Init/Prelude.lean#L1972), but we don't ship oleans from the Init package as these come with the toolchain. Co-authored-by: Mario Carneiro <[email protected]>
1 parent 1fe92bf commit d574737

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Diff for: Cache/IO.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ def CURLBIN :=
6969

7070
/-- leantar version at https://github.com/digama0/leangz -/
7171
def LEANTARVERSION :=
72-
"0.1.7"
72+
"0.1.8"
7373

7474
def EXE := if System.Platform.isWindows then ".exe" else ""
7575

0 commit comments

Comments
 (0)