…comments

Merge skip-already-unpacked-cache (leanprover-community#34667) into pipeline-cache-decompression (leanprover-community#32987) and:

- Remove duplicate hex parsing functions, use shared Char.hexDigitToNat? and
  String.parseHexToUInt64? from Cache/Lean.lean
- Use FilePath instead of String for hashFromFileName and mathlibDepPath
  (call .toString only when needed for JSON)
- Add docstring noting harvestDecompTask returns (successful, failed) tuple
- Fix typo: print stdout not stderr for lake stdout

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <[email protected]>

This PR adds pre-filtering to `lake exe cache get`: before calling leantar, we check if each module's trace file exists and has a matching Lake depHash. Modules that are already correctly unpacked are skipped entirely.

**Performance (tested on Mac Studio with SSD, ~7900 cached files):**

| Scenario | Before | After |
|----------|--------|-------|
| All files already unpacked | ~25s | ~5s |
| Partial decompression needed | ~25s | ~5s + decompression time |

**Timing breakdown (after this PR):**
- Hash computation: ~2.8s
- Filter to existing ltar files: ~0.06s  
- Read ltar headers + trace files, compare hashes: ~2.5s
- leantar (if needed): 0s when all files match

**What changed:**
Before calling leantar, we now read the Lake depHash from each ltar file header (first 12 bytes) and compare with the trace file's `depHash` field. Files with matching hashes are filtered out.

Note: The mathlib cache hash (ltar filename) is different from the Lake depHash (stored in ltar header and trace file). This PR compares the Lake depHashes, which is what leantar uses internally.

Fixes https://leanprover.zulipchat.com/#narrow/channel/536994-ecosystem-infrastructure/topic/lake.20exe.20cache.20get.20always.20decompresses

🤖 Prepared with Claude Code

This PR adds pre-filtering to `lake exe cache get`: before calling leantar, we check if each module's trace file exists and has a matching Lake depHash. Modules that are already correctly unpacked are skipped entirely.

**Performance (tested on Mac Studio with SSD, ~7900 cached files):**

| Scenario | Before | After |
|----------|--------|-------|
| All files already unpacked | ~25s | ~5s |
| Partial decompression needed | ~25s | ~5s + decompression time |

**Timing breakdown (after this PR):**
- Hash computation: ~2.8s
- Filter to existing ltar files: ~0.06s  
- Read ltar headers + trace files, compare hashes: ~2.5s
- leantar (if needed): 0s when all files match

**What changed:**
Before calling leantar, we now read the Lake depHash from each ltar file header (first 12 bytes) and compare with the trace file's `depHash` field. Files with matching hashes are filtered out.

Note: The mathlib cache hash (ltar filename) is different from the Lake depHash (stored in ltar header and trace file). This PR compares the Lake depHashes, which is what leantar uses internally.

Fixes https://leanprover.zulipchat.com/#narrow/channel/536994-ecosystem-infrastructure/topic/lake.20exe.20cache.20get.20always.20decompresses

🤖 Prepared with Claude Code

…cache is skipped (#35389)

Currently some PRs sent to `bors` have ended up failing (#35330, #34667) because the upload_cache step was skipped, causing the required Post-Build and Post-CI jobs to get skipped as well. This PR adjusts the conditionals to ensure that those steps still run even if the cache upload gets skipped.

Co-authored-by: Bryan Gin-ge Chen <[email protected]>

…cache is skipped (leanprover-community#35389)

Currently some PRs sent to `bors` have ended up failing (leanprover-community#35330, leanprover-community#34667) because the upload_cache step was skipped, causing the required Post-Build and Post-CI jobs to get skipped as well. This PR adjusts the conditionals to ensure that those steps still run even if the cache upload gets skipped.

Co-authored-by: Bryan Gin-ge Chen <[email protected]>

…cache is skipped (leanprover-community#35389)

Currently some PRs sent to `bors` have ended up failing (leanprover-community#35330, leanprover-community#34667) because the upload_cache step was skipped, causing the required Post-Build and Post-CI jobs to get skipped as well. This PR adjusts the conditionals to ensure that those steps still run even if the cache upload gets skipped.

Co-authored-by: Bryan Gin-ge Chen <[email protected]>

…r-community#34667)

This PR adds pre-filtering to `lake exe cache get`: before calling leantar, we check if each module's trace file exists and has a matching Lake depHash. Modules that are already correctly unpacked are skipped entirely.

**Performance (tested on Mac Studio with SSD, ~7900 cached files):**

| Scenario | Before | After |
|----------|--------|-------|
| All files already unpacked | ~25s | ~5s |
| Partial decompression needed | ~25s | ~5s + decompression time |

**Timing breakdown (after this PR):**
- Hash computation: ~2.8s
- Filter to existing ltar files: ~0.06s  
- Read ltar headers + trace files, compare hashes: ~2.5s
- leantar (if needed): 0s when all files match

**What changed:**
Before calling leantar, we now read the Lake depHash from each ltar file header (first 12 bytes) and compare with the trace file's `depHash` field. Files with matching hashes are filtered out.

Note: The mathlib cache hash (ltar filename) is different from the Lake depHash (stored in ltar header and trace file). This PR compares the Lake depHashes, which is what leantar uses internally.

Fixes https://leanprover.zulipchat.com/#narrow/channel/536994-ecosystem-infrastructure/topic/lake.20exe.20cache.20get.20always.20decompresses

🤖 Prepared with Claude Code

…cache is skipped (leanprover-community#35389)

Currently some PRs sent to `bors` have ended up failing (leanprover-community#35330, leanprover-community#34667) because the upload_cache step was skipped, causing the required Post-Build and Post-CI jobs to get skipped as well. This PR adjusts the conditionals to ensure that those steps still run even if the cache upload gets skipped.

Co-authored-by: Bryan Gin-ge Chen <[email protected]>

…r-community#34667)

This PR adds pre-filtering to `lake exe cache get`: before calling leantar, we check if each module's trace file exists and has a matching Lake depHash. Modules that are already correctly unpacked are skipped entirely.

**Performance (tested on Mac Studio with SSD, ~7900 cached files):**

| Scenario | Before | After |
|----------|--------|-------|
| All files already unpacked | ~25s | ~5s |
| Partial decompression needed | ~25s | ~5s + decompression time |

**Timing breakdown (after this PR):**
- Hash computation: ~2.8s
- Filter to existing ltar files: ~0.06s  
- Read ltar headers + trace files, compare hashes: ~2.5s
- leantar (if needed): 0s when all files match

**What changed:**
Before calling leantar, we now read the Lake depHash from each ltar file header (first 12 bytes) and compare with the trace file's `depHash` field. Files with matching hashes are filtered out.

Note: The mathlib cache hash (ltar filename) is different from the Lake depHash (stored in ltar header and trace file). This PR compares the Lake depHashes, which is what leantar uses internally.

Fixes https://leanprover.zulipchat.com/#narrow/channel/536994-ecosystem-infrastructure/topic/lake.20exe.20cache.20get.20always.20decompresses

🤖 Prepared with Claude Code

…cache is skipped (leanprover-community#35389)

Currently some PRs sent to `bors` have ended up failing (leanprover-community#35330, leanprover-community#34667) because the upload_cache step was skipped, causing the required Post-Build and Post-CI jobs to get skipped as well. This PR adjusts the conditionals to ensure that those steps still run even if the cache upload gets skipped.

Co-authored-by: Bryan Gin-ge Chen <[email protected]>

This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.

Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.

🤖 Prepared with Claude Code

- [x] depends on: #34667

…-community#32987)

This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.

Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.

🤖 Prepared with Claude Code

- [x] depends on: leanprover-community#34667

…-community#32987)

This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.

Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.

🤖 Prepared with Claude Code

- [x] depends on: leanprover-community#34667

…-community#32987)

This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.

Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.

🤖 Prepared with Claude Code

- [x] depends on: leanprover-community#34667

…-community#32987)

This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first.

Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O.

🤖 Prepared with Claude Code

- [x] depends on: leanprover-community#34667