Skip to content

fix: do not let elan-init modify the runner's persistent PATH #189

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
austinletson merged 2 commits into from
Oct 12, 2026
Merged

fix: do not let elan-init modify the runner's persistent PATH #189

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9b91ab0
fix: do not let elan-init modify the runner's persistent PATH
chris-dare-dev Sep 19, 2026
ca9d0f7
Merge branch 'main' into fix/elan-init-no-modify-path
austinletson Oct 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## Unreleased

### Fixed

- pass `--no-modify-path` to `elan-init` so installing elan no longer edits the
runner's persistent environment (`HKCU\Environment\PATH` on Windows,
`~/.profile` and friends elsewhere). `lean-action` already puts
`$HOME/.elan/bin` on `$GITHUB_PATH`, so this is a no-op on GitHub-hosted
runners; on self-hosted runners it stops every job from accumulating PATH
entries that outlive it
## v1.6.2 - 2026-10-12

### Fixed
Expand Down
7 changes: 6 additions & 1 deletion scripts/install_elan.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,13 @@ set -e
echo "::group::Elan Installation Output"

set -o pipefail
# `--no-modify-path` because this script puts `$HOME/.elan/bin` on `$GITHUB_PATH`
# itself, two lines below. Without the flag elan additionally edits the user's
# persistent environment -- `HKCU\Environment\PATH` on Windows, `~/.profile` and
# friends elsewhere -- which is redundant on GitHub-hosted runners and outlives
# the job on self-hosted ones.
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf |
sh -s -- -y --default-toolchain none
sh -s -- -y --default-toolchain none --no-modify-path
rm -f elan-init

echo "$HOME/.elan/bin" >>"$GITHUB_PATH"
Expand Down
Loading