From 9b91ab0d8f2ca15d56818ca3b8b514752662035f Mon Sep 17 00:00:00 2001
From: Chris Dare <cedare96@gmail.com>
Date: Sat, 19 Sep 2026 19:06:44 -0400
Subject: [PATCH] fix: do not let elan-init modify the runner's persistent PATH

`install_elan.sh` already puts `$HOME/.elan/bin` on `$GITHUB_PATH`, so the
additional persistent-environment edit elan-init performs by default is
redundant on GitHub-hosted runners and harmful on self-hosted ones.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 CHANGELOG.md            | 9 +++++++++
 scripts/install_elan.sh | 7 ++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 28e88ee..a133104 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,15 @@ 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.0 - 2026-08-22
 
 ### Added
diff --git a/scripts/install_elan.sh b/scripts/install_elan.sh
index ad678c4..f8167ca 100755
--- a/scripts/install_elan.sh
+++ b/scripts/install_elan.sh
@@ -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"