feat: use `leantar` in `lake exe cache` #5710

digama0 · 2023-07-04T09:29:20Z

This hooks up the new leantar tool from https://github.com/digama0/leangz to lake exe cache. It uses an olean compressor to achieve much smaller file sizes, and faster decompression. See the Zulip discussion.

The new files have a new file extension, 123.ltar instead of 123.tar.gz. This implementation does not multiplex between them, so it will be a hard reset. In fact, the new cache doesn't even know how to clear the old cache files, so you might need to do that manually. Switching between branches will still work during the interim, since the cache will have both kinds of file and use the right ones.

depends on: [Merged by Bors] - chore: bump to nightly-2023-07-01 #5409

Cache/IO.lean

semorrison · 2023-07-04T23:30:48Z

All working for me now, and a massive speedup:

# Before #5710
lake clean && lake exe cache get!   # 343s
lake exe cache get                  # 17s

# After #5710
lake clean && lake exe cache get!   # 49s
lake exe cache get                  # 4s

digama0 · 2023-07-11T04:26:15Z

Oh wow, I just had the pleasure of running lake exe cache get on a low bandwidth hotel wifi, and it took 25 minutes. A (projected) 7x decrease to 3.57 minutes would make quite a big difference!

semorrison · 2023-07-13T02:30:48Z

This PR/issue depends on:

~~[Merged by Bors] - chore: bump to nightly-2023-07-01 #5409~~
By Dependent Issues (🤖). Happy coding!

semorrison · 2023-07-13T04:47:17Z

bors merge

This hooks up the new `leantar` tool from https://github.com/digama0/leangz to `lake exe cache`. It uses an olean compressor to achieve much smaller file sizes, and faster decompression. See the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/leangz.3A.20olean.20file.20compressor/near/369738648). The new files have a new file extension, `123.ltar` instead of `123.tar.gz`. This implementation does not multiplex between them, so it will be a hard reset. In fact, the new cache doesn't even know how to clear the old cache files, so you might need to do that manually. Switching between branches will still work during the interim, since the cache will have both kinds of file and use the right ones.

bors · 2023-07-13T06:08:59Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

This reverts commit 6ed1d66.

This reverts commit 6ed1d66. Currently broken on gitpod (needs `sudo apt-get install xz-utils`) and on Windows (likely the same issue). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Cache/IO.lean

gebner · 2023-07-15T06:47:42Z

Cache/IO.lean

+    s!"https://github.com/digama0/leangz/releases/download/v{LEANTARVERSION}/leantar-v{LEANTARVERSION}-{target}.{ext}",
+    "-L", "-o", s!"{LEANTARBIN}.{ext}"]
+  let _ ← runCmd "tar" #["-xf", s!"{LEANTARBIN}.{ext}",
+    "-C", IO.CACHEDIR.toString, "--strip-components=1"]


Does this work on windows (i.e., with zip)?

It seems to work... not sure how universally available tar is on windows but this exact command was tested and works on at least a few machines. (The old cache was also using tar for unpacking on windows and I don't think we have received any complaints about it.)

😱

The old cache was also using tar for unpacking on windows and I don't think we have received any complaints about it.

The old cache used tar to unpack tar files. This line here uses tar to unpack zip files. But if it works. 🤷

gebner · 2023-07-15T06:50:10Z

I am happy with the static linking issue now. The branch works fine on nixos.

@fpvandoorn complained about windows performance on zulip. Is this still an issue (is it even a regression) and is there something we can do about it?

digama0 · 2023-07-15T06:59:40Z

We investigated it and it doesn't seem like there is much we can do about it, the bottleneck is the write itself and I think windows is just slow at writing lots of files. I don't think it is a regression compared to the original tar script, but perhaps @fpvandoorn could do a clean test and confirm this.

fpvandoorn · 2023-07-15T08:17:20Z

When testing a bit more carefully yesterday, I think now that leantar is still quite a bit quicker than the original tar. I don't have time to test it atm, but I'm happy if this gets merged.

gebner · 2023-07-15T16:33:03Z

bors r+

bors · 2023-07-15T16:33:05Z

Already running a review

semorrison · 2023-07-17T20:26:07Z

bors seems to not be working. I'll try again.

semorrison · 2023-07-17T20:26:12Z

bors r-

semorrison · 2023-07-17T20:27:46Z

bors merge

bors · 2023-07-17T20:27:47Z

Already running a review

Seems to be resolved, and I'm dismissing this in case it is interacting with the strange bors behaviour.

semorrison · 2023-07-17T22:09:23Z

I think bors is failing here because it has already merged this PR once (my fault, I merged too early and had to revert). I'm just going to squash merge now.

This hooks up the new `leantar` tool from https://github.com/digama0/leangz to `lake exe cache`. It uses an olean compressor to achieve much smaller file sizes, and faster decompression. See the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/leangz.3A.20olean.20file.20compressor/near/369738648). The new files have a new file extension, `123.ltar` instead of `123.tar.gz`. This implementation does not multiplex between them, so it will be a hard reset. In fact, the new cache doesn't even know how to clear the old cache files, so you might need to do that manually. Switching between branches will still work during the interim, since the cache will have both kinds of file and use the right ones.

This reverts commit 6ed1d66. Currently broken on gitpod (needs `sudo apt-get install xz-utils`) and on Windows (likely the same issue). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* feat: use `leantar` in `lake exe cache` * run pack in parallel * bump leantar * version check * use hex for hashes * chore: bump to 0.1.2, add .exe on windows * fix: file extension on linux * fix: arch is reported as arm64 sometimes * fix: statically linked 0.1.3

feat: use leantar in lake exe cache

77e7b95

digama0 added the awaiting-review label Jul 4, 2023

semorrison reviewed Jul 4, 2023

View reviewed changes

Cache/IO.lean Outdated Show resolved Hide resolved

digama0 added 4 commits July 4, 2023 07:15

run pack in parallel

220f5db

bump leantar

52c9f47

version check

b1c348e

use hex for hashes

442de34

semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Jul 4, 2023

semorrison added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. blocked-by-other-PR This PR depends on another PR to Mathlib labels Jul 11, 2023

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 13, 2023

bors bot changed the title ~~feat: use leantar in lake exe cache~~ [Merged by Bors] - feat: use leantar in lake exe cache Jul 13, 2023

bors bot closed this Jul 13, 2023

bors bot deleted the leantar branch July 13, 2023 06:09

semorrison added a commit that referenced this pull request Jul 13, 2023

chore: revert leantar #5710 for further testing

3989b67

This reverts commit 6ed1d66.

semorrison restored the leantar branch July 13, 2023 07:22

semorrison reopened this Jul 13, 2023

semorrison changed the title ~~[Merged by Bors] - feat: use leantar in lake exe cache~~ feat: use leantar in lake exe cache Jul 13, 2023

semorrison added awaiting-review and removed ready-to-merge This PR has been sent to bors. labels Jul 13, 2023

chore: bump to 0.1.2, add .exe on windows

6b22a3e

digama0 added 3 commits July 13, 2023 14:47

Merge branch 'master' into leantar

ed43cd0

fix: file extension on linux

2668c20

fix: arch is reported as arm64 sometimes

588f203

gebner previously requested changes Jul 13, 2023

View reviewed changes

Cache/IO.lean Outdated Show resolved Hide resolved

fix: statically linked 0.1.3

2b48dd0

digama0 requested a review from gebner July 14, 2023 21:32

gebner reviewed Jul 15, 2023

View reviewed changes

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 15, 2023

semorrison added awaiting-review and removed ready-to-merge This PR has been sent to bors. labels Jul 17, 2023

semorrison merged commit ede7b29 into master Jul 17, 2023
28 checks passed

bors bot deleted the leantar branch July 17, 2023 22:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: use `leantar` in `lake exe cache` #5710

feat: use `leantar` in `lake exe cache` #5710

digama0 commented Jul 4, 2023 •

edited by github-actions bot

Loading

semorrison commented Jul 4, 2023

digama0 commented Jul 11, 2023

semorrison commented Jul 13, 2023

semorrison commented Jul 13, 2023

bors bot commented Jul 13, 2023

gebner Jul 15, 2023

digama0 Jul 15, 2023 •

edited

Loading

gebner Jul 15, 2023

gebner commented Jul 15, 2023

digama0 commented Jul 15, 2023

fpvandoorn commented Jul 15, 2023

gebner commented Jul 15, 2023

bors bot commented Jul 15, 2023

semorrison commented Jul 17, 2023

semorrison commented Jul 17, 2023

semorrison commented Jul 17, 2023

bors bot commented Jul 17, 2023

semorrison commented Jul 17, 2023

feat: use leantar in lake exe cache #5710

feat: use leantar in lake exe cache #5710

Conversation

digama0 commented Jul 4, 2023 • edited by github-actions bot Loading

semorrison commented Jul 4, 2023

digama0 commented Jul 11, 2023

semorrison commented Jul 13, 2023

semorrison commented Jul 13, 2023

bors bot commented Jul 13, 2023

gebner Jul 15, 2023

Choose a reason for hiding this comment

digama0 Jul 15, 2023 • edited Loading

Choose a reason for hiding this comment

gebner Jul 15, 2023

Choose a reason for hiding this comment

gebner commented Jul 15, 2023

digama0 commented Jul 15, 2023

fpvandoorn commented Jul 15, 2023

gebner commented Jul 15, 2023

bors bot commented Jul 15, 2023

semorrison commented Jul 17, 2023

semorrison commented Jul 17, 2023

semorrison commented Jul 17, 2023

bors bot commented Jul 17, 2023

semorrison commented Jul 17, 2023

feat: use `leantar` in `lake exe cache` #5710

feat: use `leantar` in `lake exe cache` #5710

digama0 commented Jul 4, 2023 •

edited by github-actions bot

Loading

digama0 Jul 15, 2023 •

edited

Loading