Skip to content

fix(runtimes): rely on AWF_HOST_PATH for Lean toolchain discovery#350

Closed
Copilot wants to merge 2 commits into
mainfrom
copilot/check-lean-installation
Closed

fix(runtimes): rely on AWF_HOST_PATH for Lean toolchain discovery#350
Copilot wants to merge 2 commits into
mainfrom
copilot/check-lean-installation

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Apr 28, 2026

The Lean runtime's install step couldn't be found by the agent inside AWF. The original code installed elan to $HOME/.elan and then symlinked the wrappers into /tmp/awf-tools/ on the assumption that $HOME wasn't reachable from the sandbox — but the symlinks dangle because the wrappers re-exec into $HOME/.elan/toolchains/....

AWF actually captures the host runner's PATH (plus $GITHUB_PATH entries) into AWF_HOST_PATH and re-exports it as PATH inside the chroot, so ##vso[task.prependpath] is sufficient.

Summary

  • src/runtimes/lean/mod.rs — install elan to its default $HOME/.elan location and ##vso[task.prependpath] $HOME/.elan/bin. Drops the mkdir -p /tmp/awf-tools + symlink loop.
  • src/runtimes/lean/extension.rs, docs/runtimes.md — note that Lean is on PATH inside the sandbox via AWF_HOST_PATH; no absolute-path guidance needed.
curl https://elan.lean-lang.org/elan-init.sh -sSf \
  | sh -s -- -y --default-toolchain stable
echo "##vso[task.prependpath]$HOME/.elan/bin"

Test plan

  • cargo test (existing test_lean_prepare_steps still asserts elan-init.sh is present)
  • cargo clippy --all-targets --all-features

Copilot AI and others added 2 commits April 28, 2026 21:40
@jamesadevine
Copy link
Copy Markdown
Collaborator

This was pants and not the root cause.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants