From ae792b163b49306c8989b7e964c3d0c85fb7fc54 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 27 May 2026 14:25:42 +0000 Subject: [PATCH 1/2] fix: canonicalize `toolchains_dir` when checking if inside a toolchain (#161) Fixes #161. On Windows, `fs::canonicalize` normalizes the drive-letter case (and prepends the `\\?\` UNC prefix), but `self.toolchains_dir` is built from the raw `ELAN_HOME` / `HOME` env var and never canonicalized. If `cwd` is reported as e.g. `c:\...` (lowercase), the canonicalized walked-up `dir` becomes `\\?\\C:\...` while `self.toolchains_dir` stays `c:\...`, the equality fails, and elan never recognizes the user is inside a toolchain directory. --- CHANGELOG.md | 4 ++++ src/elan/config.rs | 49 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 10bb7ea..9c5a6d7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +# Unreleased + +- Fix detection of being inside a toolchain directory on Windows when the path is reported with a lowercase drive letter (#199). + # 4.2.1 - 2026-03-18 - Fix combining `elan override` with new path-based toolchains. diff --git a/src/elan/config.rs b/src/elan/config.rs index 4c7b649..4465818 100644 --- a/src/elan/config.rs +++ b/src/elan/config.rs @@ -224,7 +224,9 @@ impl Cfg { dir = d.parent(); - if dir == Some(&self.toolchains_dir) { + // NOTE: `dir` is already canonicalized, so `==` should be good here + let toolchains_dir = utils::canonicalize_path(&self.toolchains_dir, &|n| notify(n.into())); + if dir == Some(&*toolchains_dir) { if let Some(last) = d.file_name() { if let Some(last) = last.to_str() { return Ok(Some(( @@ -368,3 +370,48 @@ impl Cfg { toolchain.open_docs(relative) } } + +#[cfg(test)] +mod tests { + use super::*; + use std::fs; + use tempfile::TempDir; + + fn make_cfg(elan_dir: PathBuf, toolchains_dir: PathBuf) -> Cfg { + Cfg { + settings_file: SettingsFile::new(elan_dir.join("settings.toml")), + temp_cfg: temp::Cfg::new(elan_dir.join("tmp"), Box::new(|_| {})), + elan_dir, + toolchains_dir, + env_override: None, + notify_handler: Arc::new(|_| {}), + } + } + + // Regression test for #161: on Windows, `cwd` can come back with a + // lowercase `c:` while `self.toolchains_dir` (built from env vars) has + // `C:`, so the raw equality check failed and elan didn't recognize the + // user was inside a toolchain. We simulate the same canonical-vs-raw + // mismatch on Linux by giving `toolchains_dir` extra `..` components. + #[test] + fn detects_inside_toolchain_dir_when_toolchains_dir_path_is_not_canonical() { + let elan = TempDir::new().unwrap(); + let tc_dir = elan + .path() + .join("toolchains") + .join("leanprover--lean4---v4.0.0"); + fs::create_dir_all(&tc_dir).unwrap(); + + let toolchains_dir = elan.path().join("toolchains").join("..").join("toolchains"); + let cfg = make_cfg(elan.path().to_path_buf(), toolchains_dir); + + let result = cfg + .find_override_from_dir_walk(&tc_dir, &Settings::default()) + .unwrap(); + + match result { + Some((_, OverrideReason::InToolchainDirectory(_))) => {} + other => panic!("expected InToolchainDirectory, got {other:?}"), + } + } +} From 069b7ed52f176eed9c6bae14e6f1db4bd36a662d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 27 May 2026 14:47:54 +0000 Subject: [PATCH 2/2] docs: track CLAUDE.md with codebase guidance for Claude Code --- CLAUDE.md | 145 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 CLAUDE.md diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..a59adcc --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,145 @@ +# CLAUDE.md + +This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. + +## Project Overview + +**elan** is a toolchain version manager for the Lean theorem prover, forked from rustup. It manages multiple Lean installations and automatically selects the correct version based on `lean-toolchain` files in projects. The binary is a chimera that changes behavior based on its invocation name: +- `elan`/`elan-init`: Main CLI application and installer +- `lean`, `lake`, etc.: Proxies that delegate to the correct toolchain version + +## Build Commands + +### Basic Build +```bash +cargo build +# Output: target/debug/elan-init +``` + +### Release Build +```bash +cargo build --release +# Output: target/release/elan-init +``` + +### Cross-compilation (used in CI) +```bash +cargo install cross --locked +cross build --release --target +# Examples: x86_64-unknown-linux-musl, aarch64-apple-darwin, x86_64-pc-windows-msvc +``` + +### Testing +```bash +cargo test --release --target +``` + +### Windows Build Requirements +- 64-bit developer command prompt +- Windows version of perl.exe from https://strawberryperl.com/ (must be first in PATH, not Git's perl) + +## Architecture + +### Binary Dispatch (src/elan-cli/main.rs) +The main entry point determines behavior by examining arg0: +- `elan` → `elan_mode::main()` - CLI commands +- `elan-init` / `elan-setup*` → `setup_mode::main()` - Installation +- `elan-gc-*` → `self_update::complete_windows_uninstall()` - Windows cleanup +- Any other name → `proxy_mode::main()` - Tool proxying (lean, lake, etc.) + +Recursion guard via `LEAN_RECURSION_COUNT` environment variable prevents infinite proxy loops. + +### Workspace Structure +This is a Cargo workspace with four crates: +- `elan` (src/elan/lib.rs): Core library with config, toolchain resolution, and installation logic +- `elan-init` (src/elan-cli/): Main binary and CLI implementation +- `elan-dist` (src/elan-dist/): Distribution management, manifests, and component installation +- `elan-utils` (src/elan-utils/): Shared utilities +- `download` (src/download/): HTTP download functionality (curl-backend or reqwest-backend) + +### Key Concepts + +**Toolchain Resolution** (src/elan/toolchain.rs, src/elan/config.rs): +- Toolchain descriptors can be: + - `Remote`: Downloaded from GitHub releases (e.g., `leanprover/lean4:v4.0.0`) + - `Local`: Custom linked toolchains +- Resolution hierarchy checks (in order): + 1. `ELAN_TOOLCHAIN` environment variable + 2. Directory override (`elan override set`) + 3. `lean-toolchain` file in current/parent directories + 4. `leanpkg.toml` file (legacy) + 5. Inside a toolchain directory itself + 6. Default toolchain from settings + +**Proxy Mode** (src/elan-cli/proxy_mode.rs): +When elan is called as `lean`, `lake`, etc., it: +1. Checks for `+toolchain` as first argument for explicit toolchain selection +2. Resolves which toolchain to use for current directory +3. Executes the real binary from that toolchain's directory + +**Configuration** (src/elan/config.rs): +- ELAN_HOME: `~/.elan` (configurable) +- Settings file: `~/.elan/settings.toml` (default toolchain, overrides) +- Toolchains directory: `~/.elan/toolchains/` +- Temporary directory: `~/.elan/tmp/` + +### CLI Commands (src/elan-cli/elan_mode.rs) +Main commands implemented: +- `show`: Display active and installed toolchains +- `install/uninstall`: Manage toolchains +- `default`: Set default toolchain +- `override set/unset/list`: Per-directory toolchain overrides +- `toolchain link`: Create custom toolchain from local directory +- `toolchain gc`: Garbage-collect unused toolchains +- `run`: Run command with specific toolchain +- `which`: Show path to binary +- `doc/man`: Open documentation +- `self update/uninstall`: Manage elan itself +- `completions`: Generate shell completions + +### Download Backend +Two features control HTTP backend (default: curl-backend): +- `curl-backend`: Uses libcurl +- `reqwest-backend`: Pure Rust alternative + +### Feature Flags +- `no-self-update`: Disable self-update functionality (for package managers) +- `msi-installed`: Changes self-update/uninstall behavior for Windows MSI installations + +## Installation Flow +1. `elan-init.sh` or `elan-init.ps1` downloads and runs `elan-init` binary +2. Setup mode installs to `~/.elan`, adds to PATH via shell config +3. Creates symlinks: `elan`, `lean`, `lake` → `elan-init` +4. Downloads default toolchain on first use + +## Commit Messages + +Write the subject as `: (#)` (e.g. `fix: path-based toolchain as override (#195)`). A body is optional; when present, separate it from the subject with a blank line and write each paragraph as one long line — do not hard-wrap inside a paragraph. Blank lines between paragraphs are fine. + +## Changelog + +User-facing fixes and features must add a bullet to `CHANGELOG.md` in the same commit. Add to (or create) the top `# Unreleased` section — at release time it becomes `# X.Y.Z - YYYY-MM-DD`. Pure internal refactors, test-only changes, and `chore:` commits don't need an entry. + +## Testing Strategy +No unit tests (marked `test = false` in Cargo.toml). Integration testing via: +- CI runs build, test, and install test on all platforms +- Install test: runs `elan-init -y`, creates new lake project, builds it + +## Development Notes + +### Rustup Legacy +This codebase is a fork of rustup with terminology changes: +- rustup → elan +- cargo → lake +- rust(c) → lean +- CARGO_HOME merged with RUSTUP_HOME + +### Toolchain Naming +Toolchains follow pattern: `[origin/][owner/repo:]release` +- Default origin: `leanprover/lean4` (becomes `leanprover/lean4-nightly` for nightly builds) +- Nightly releases: `nightly-YYYY-MM-DD` +- Stable releases: `vX.Y.Z` or `X.Y.Z` (auto-prefixed with `v`) +- Special channels: `stable`, `beta`, `nightly`, `lean-toolchain` (resolve to latest local) + +### NixOS Support +Toolchains require patching on NixOS - handled by Nixpkgs version. See `fetch_nixos_patch.sh`.