Windows Elan Install: Core Files Missing

Stream: general

[Albert Pacelli]

Subject: Persistent Lean 4 Toolchain Installation Failure on Windows - Core Files Missing (lean.exe, .olean files)

Hi everyone,

I'm encountering a persistent issue with installing a complete Lean 4 toolchain on my Windows system using elan, and I'd greatly appreciate any insights or help.

The Core Problem:

Despite elan reporting successful downloads and installations for various toolchains (including stable which is v4.19.0, v4.18.0, and the latest nightly-2025-05-17), critical files are consistently missing from the installed toolchain directories.

Specifically:

1. The main lean.exe executable is missing from its expected location within the toolchain (e.g., C:\Users\appac\.elan\toolchains\leanprover--lean4---v4.19.0\bin\lean.exe).

2. Core standard library compiled files like Format.olean are missing from the lib\lean\Std\ directory of the installed toolchains.

Key Error Message (when trying to run Lean via the elan shim):

When I try to run lean --version (after elan setup), and the shim C:\Users\appac\.elan\bin\lean.exe executes, I get:

error: toolchain 'leanprover/lean4:v4.19.0' does not have the binary C:\Users\appac\.elan\toolchains\leanprover--lean4---v4.19.0\bin\lean.exe

This confirms the actual Lean executable is not being placed correctly within the toolchain directory.

Troubleshooting Steps Already Taken:

We've gone through an extensive troubleshooting process, including:

• Multiple attempts to install different toolchains (stable/v4.19.0, v4.18.0, nightly).

• Running all elan commands (elan self uninstall, elan toolchain install, elan default, elan-init.ps1) from an Administrator Command Prompt.

• Completely reinstalling elan: This involved elan self uninstall, manually deleting the entire C:\Users\appac\.elan folder (after a reboot to release file locks), and then re-running elan-init.ps1 (downloaded from the official GitHub raw link).

• Temporarily disabling Windows Defender's Real-time protection during the elan toolchain install steps.

• Ensuring the PATH environment variable for my user includes %USERPROFILE%\.elan\bin (and C:\Users\appac\.elan\bin appears correctly when I echo %PATH%).

• Confirmed that the shim executables (elan.exe, lean.exe, lake.exe) are present in C:\Users\appac\.elan\bin.

• During earlier uninstallation attempts (before consistently using admin rights from a neutral directory like C:\), I encountered "Access is denied (os error 5)" and "File in use (os error 32)" errors, which seemed to be resolved by the admin/neutral directory approach for the uninstall command itself.

Current Hypothesis:

The issue seems to be that elan successfully downloads the toolchain archive (.tar.zst file), but something on my specific Windows system is preventing it from correctly and completely extracting or placing all the necessary files (both executables and .olean library files) into the respective toolchain directory (e.g., C:\Users\<my_username>\.elan\toolchains\leanprover--lean4---v4.19.0\), even when elan reports the installation as "successful."

I'm at a point where I suspect an environment-specific issue that's interfering with elan's file operations during the extraction phase.

Could anyone offer suggestions for further diagnostics, or has anyone encountered a similar situation where elan fails to populate the toolchain directory fully on Windows despite no explicit error during the elan toolchain install command itself? Are there verbose logging options for elan's extraction process?

Any help would be greatly appreciated!

Thank you.