[chris-dare-dev]

scripts/install_elan.sh runs the elan installer on every job without
--no-modify-path:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf |
  sh -s -- -y --default-toolchain none

Two lines later the same script does the thing GitHub Actions actually wants:

echo "$HOME/.elan/bin" >>"$GITHUB_PATH"

So lean-action is already responsible for making lean and lake resolve in
later steps, and the persistent-environment edit elan-init performs on top of
that is redundant. On GitHub-hosted runners it is harmless, because the VM is
discarded. On self-hosted runners it is not: it permanently mutates the account
that runs the jobs.

What the default does on Windows

do_add_to_path in elan opens HKCU\Environment, prepends $ELAN_HOME\bin
to PATH, writes it back as REG_EXPAND_SZ and broadcasts WM_SETTINGCHANGE.
no_modify_path is a clap flag in src/elan-cli/setup_mode.rs and is read from
nowhere else, so there is no environment variable a runner operator can set to
opt out. Setting ELAN_HOME does not help either — it only changes which path
gets written.

On Linux and macOS the same default appends an export PATH=... line to
~/.profile (and ~/.bash_profile/~/.zprofile when present), so self-hosted
runners there have a smaller version of the same problem.

Why it matters on self-hosted runners

Concretely, on a Windows box running four self-hosted runners, each with its own
ELAN_HOME so that concurrent jobs do not contend over one toolchain:

1. Every job prepends C:\actions-runner\<runner>\.elan\bin to the operator's
   user PATH. Because elan prepends, those entries land ahead of the
   operator's own ~\.elan\bin.

2. An interactive lake then resolves to a runner's shim, and
   .elan\bin\lake.exe stays open for the duration of that build.

3. elan installs its shims as hardlinks to a single elan.exe, and the next job
   on that runner re-runs the installer, which tries to recreate the link set.
   Windows will not relink a running image, so the job fails about 24 seconds in
   with:

   error: could not create link from '<runner>\.elan\bin\elan.exe'
                                  to '<runner>\.elan\bin\lake.exe'
   

4. That posts a red required check on whatever PR happened to be queued.

The operator cannot fix this from their side: stripping the entries only lasts
until the next job re-adds them, ELAN_HOME/HOME do not suppress the write,
and reordering PATH does not help because elan prepends.

The change

Pass --no-modify-path. The flag is accepted by elan-init.sh, which forwards
its arguments verbatim to the downloaded binary.

Nothing in the action depends on the behaviour being removed: install_elan.sh
invokes lean/lake by absolute path within its own step, and every later
script (config.sh, lake_build.sh, …) calls bare lake/elan, which resolve
through the $GITHUB_PATH entry this script writes.

Verification

On Windows, against current elan, with a throwaway ELAN_HOME:

• without --no-modify-path: HKCU\Environment\PATH gains the
  $ELAN_HOME\bin entry at position 1.
• with --no-modify-path: elan installs normally (lean --version and
  lake --version both succeed) and HKCU\Environment\PATH is byte-identical
  before and after.

Notes

No functional test is added. The behaviour this removes is invisible on
GitHub-hosted runners by construction, so a test would only re-assert that
lean and lake still resolve in later steps — which the existing functional
tests already cover, and which is the actual regression risk here. Happy to add
a Windows test that snapshots HKCU\Environment\PATH across the action if you
would like one.

[austinletson]

Thanks for the fix!