Lake release fetch can fail on Windows Chinese locale because tar -xvvz output is not valid UTF-8

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Notes:

• I searched for related issues using terms such as non UTF-8 tar Windows Lake and Tried to read from handle containing non UTF-8 data, but did not find an existing issue.
• I have not yet reduced this to a dependency-free Lake project. The current reproducible case is mathematics_in_lean, where the failure happens during lake exe cache get.
• I have not tested this against Lean nightly locally. The live Lean environment does not seem applicable because this issue depends on Lake invoking the local Windows tar.exe.

Description

On Windows with a Chinese system locale, Lake release fetching can fail if the external tar.exe command emits output that is not valid UTF-8.

I encountered this when running lake exe cache get in mathematics_in_lean. The failure happened while fetching the ProofWidgets GitHub release build.

The archive itself does not appear to be corrupt. It can be extracted manually, and rerunning lake exe cache get may succeed after the first failed run has already extracted enough files.

The issue seems to be related to Lake invoking tar with verbose flags:

tar -xvvz -f ... -C ...

On my Windows machine, this appears to make tar.exe write output that Lake cannot decode as UTF-8. Lake then fails the release fetch with a UTF-8 decoding error.

Context

This occurred while setting up mathematics_in_lean on Windows.

Although the immediate trigger was ProofWidgets during lake exe cache get, the root issue seems more general: Lake should not fail a release fetch only because an external tool writes non-UTF-8 verbose or diagnostic output.

This is especially confusing for new users because after lake exe cache get fails, the project may fall back to building from source, which can take a long time.

Steps to Reproduce

1. Use Windows with a Chinese system locale.

2. Clone mathematics_in_lean:

git clone https://github.com/leanprover-community/mathematics_in_lean.git mil
cd mil

3. Run:

lake exe cache get

Expected behavior: Lake should fetch and extract the release artifact successfully. Non-UTF-8 verbose or diagnostic output from an external tool should not make the release fetch fail.

Actual behavior: Lake fails while executing tar, apparently because the captured output contains non-UTF-8 data.

The error is:

error: failed to execute 'tar': Tried to read from handle containing non UTF-8 data.
error: failed to fetch GitHub release
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

Versions

Lean version:

Lean (version 4.28.0, x86_64-w64-windows-gnu, commit 7e01a1bf5c70fc6167d49c345d3bf80596e9a79b, Release)

Lake version:

Lake version 5.0.0-src+7e01a1b (Lean version 4.28.0)

Project toolchain:

leanprover/lean4:v4.28.0

OS:

Microsoft Windows [Version 10.0.26200.8457]

Locale / encoding information:

(Get-Culture).Name: zh-CN

[Console]::OutputEncoding:
EncodingName: Unicode (UTF-8)
WebName: utf-8
CodePage: 65001

tar.exe used:

C:\Windows\System32\tar.exe

Additional Information

As a workaround, I put a wrapper tar.exe in the project root. The wrapper forwards to:

C:\Windows\System32\tar.exe

but changes:

-xvvz

to:

-xz

With this workaround, the first lake exe cache get succeeds.

This suggests that extraction itself is fine, and the failure is caused by verbose tar output that Lake cannot decode as UTF-8.

Possible fixes might include:

• avoid verbose vv output for untar when it is not needed;
• avoid capturing tar output when running quietly;
• handle external process output as bytes or decode it lossily instead of assuming UTF-8.

Impact

This affects Windows users with non-English system locales when Lake fetches GitHub release artifacts using tar.

In this case, it made the first lake exe cache get fail and could cause users to fall back to a slow source build.

Start with the Lake release-fetch path used by lake exe cache get, focusing on how the external tar.exe process is invoked and its output is decoded. Reproduce on Windows with a Chinese locale and verify that fetching and extracting the release succeeds when tar emits non-UTF-8 verbose output.