Title: Elan Fails to Install Complete Toolchain on Windows (Native & WSL) - Core Files Missing (e.g., lean.exe, Std/Format.olean) Despite Reporting Success

[pacellia]

Environment:
Operating System: Windows (User has tried on two separate Windows machines: a PC and a laptop, with similar results)
elan Version: Latest, installed via elan-init.ps1 after full uninstall and deletion of ~/.elan directory.
Lean Toolchains Attempted: stable (resolving to v4.19.0), v4.18.0, nightly (specifically nightly-2025-05-17, which is Lean 4.21.0-nightly), and v4.5.0.

Problem Summary:
elan consistently fails to create a complete and functional Lean 4 toolchain installation on Windows. While elan downloads the toolchain archive (e.g., .tar.zst file) and reports the installation as "successful" (e.g., leanprover/lean4:v4.19.0 installed - Lean (version 4.19.0, ...)), critical files are missing from the installed toolchain directory (%USERPROFILE%.elan\toolchains<toolchain_name>). This issue has been observed on two different Windows machines and also persists when attempting installation within a fresh WSL/Ubuntu environment on one of the PCs.

Symptoms & Error Messages:
Missing Toolchain Executable: When attempting to run lean --version after elan setup, the elan shim (%USERPROFILE%.elan\bin\lean.exe) executes but then reports:error: toolchain 'leanprover/lean4:v4.19.0' does not have the binary C:\Users<username>.elan\toolchains\leanprover--lean4---v4.19.0\bin\lean.exe (A dir command confirmed lean.exe was indeed missing from this toolchain's bin directory on the native Windows PC for v4.19.0).

Missing Standard Library .olean Files:
VS Code (with the Lean 4 extension) reports errors like: object file 'C:\Users<username>.elan\toolchains\leanprover--lean4---v4.19.0\lib\lean\Std\Data\Format.olean' of module Std.Data.Format does not exist. (Note: The import should likely be Std.Format).
Manual verification using dir in Command Prompt (Windows) or ls -l in Bash (WSL/Ubuntu) confirms that Format.olean is missing from the lib\lean\Std\ directory of the installed toolchains (v4.19.0, nightly-2025-05-17).
For v4.19.0 in WSL, other .olean files (e.g., Classes.olean, Data.olean) were present in lib/lean/Std/, but Format.olean was specifically absent. For v4.5.0 installed in WSL, the entire lib/lean/Std/ directory was missing (a cd $HOME/.elan/toolchains/leanprover--lean4---v4.5.0/lib/lean/Std/ command failed with "No such file or directory"). However, the top-level lib/ and lib/lean/ directories for v4.5.0 did exist.

Comprehensive Troubleshooting Steps Performed:
Multiple cycles of elan toolchain uninstall and elan toolchain install for various versions (stable/v4.19.0, v4.18.0, nightly, v4.5.0).
All elan commands executed from an Administrator Command Prompt (Windows) or sudo (where appropriate, though elan itself doesn't typically need sudo for user-level installs on Linux).
Full elan reinstallation: elan self uninstall.
Manual deletion of the entire %USERPROFILE%.elan directory (requiring a reboot to release file locks on Windows).
Fresh download of elan-init.ps1 from raw.githubusercontent.com and execution using powershell -ExecutionPolicy Bypass -File .\elan-init.ps1.
Windows Defender Real-time protection temporarily disabled during elan toolchain install attempts on native Windows.
Verified that %USERPROFILE%.elan\bin is correctly added to the user PATH environment variable, and echo %PATH% confirms its presence.
Verified that the elan shim executables (elan.exe, lean.exe, lake.exe) are physically present and correctly created in %USERPROFILE%.elan\bin.
The issue was reproduced on a separate Windows laptop where elan also failed to install Std/Format.olean for v4.19.0.The issue was reproduced within a fresh WSL/Ubuntu (24.04.1 LTS) environment on the primary PC. elan was installed within Ubuntu using curl ... | sh, and toolchains (v4.19.0, nightly, v4.5.0) were installed via elan toolchain install. The same pattern of missing core files (Std/Format.olean, or even the entire lib/lean/Std/ directory for v4.5.0) occurred.
Disk space is confirmed to be ample in all environments.
Encountered "Access is denied (os error 5)" and "File in use (os error 32)" during earlier elan toolchain uninstall attempts on Windows before consistently using an Administrator prompt from a neutral directory (e.g., C:).

Current Hypothesis: The core problem appears to be that elan successfully downloads the toolchain archive (e.g., lean-4.19.0-windows.tar.zst or lean-4.19.0-linux.tar.zst), but the subsequent extraction and file placement process is failing silently or incompletely on these Windows systems (both native and within WSL). It's not placing all the necessary files into the respective toolchain directory (e.g., %USERPROFILE%.elan\toolchains\leanprover--lean4---<version_string>), despite elan reporting the overall installation as "successful." The consistent absence of Std/Format.olean across multiple versions and environments is a key symptom.

Request: Could you please provide guidance on further diagnostics for elan's extraction process on Windows? Are there verbose logging options for the elan toolchain install command that might reveal errors during file extraction from the .tar.zst archive? Are there known conflicts with specific Windows configurations, other software, or issues with the unarchiving utilities elan might be using internally that could cause such partial extraction failures?

This issue is preventing any local Lean 4 development. Any assistance would be greatly appreciated.Thank you. (Please replace with your actual Windows username if needed, though I've used %USERPROFILE% where appropriate).