|
| 1 | +name: Set up elan + Lean toolchain |
| 2 | +description: > |
| 3 | + Install elan into the test-home directory (if not cached), prepend its |
| 4 | + `bin/` to `$GITHUB_PATH`, and pre-install a Lean toolchain so the |
| 5 | + download surfaces as a named CI step rather than blocking the first |
| 6 | + test invocation. Optionally sets that toolchain as the elan default. |
| 7 | + The caller is responsible for restoring/saving the elan cache around |
| 8 | + this action; cache-key choice is job-specific (resolved version for |
| 9 | + `:stable`, UTC date for `:nightly`). |
| 10 | +
|
| 11 | +inputs: |
| 12 | + channel: |
| 13 | + description: Lean toolchain channel (e.g. leanprover/lean4:stable, leanprover/lean4:nightly). |
| 14 | + required: true |
| 15 | + default: |
| 16 | + description: If `'true'`, set the channel as elan's default toolchain after install. |
| 17 | + required: false |
| 18 | + default: 'false' |
| 19 | + |
| 20 | +runs: |
| 21 | + using: composite |
| 22 | + steps: |
| 23 | + # Run the same install scripts the extension itself executes (see |
| 24 | + # `vscode-lean4/scripts/elan-install/install-{unix.sh,windows.ps1}`, |
| 25 | + # imported by `src/utils/leanInstaller.ts` via webpack `asset/source`). |
| 26 | + # Single source of truth — edit the script files and both production |
| 27 | + # and CI pick up the change. |
| 28 | + # |
| 29 | + # The scripts default-toolchain to `leanprover/lean4:stable`; callers |
| 30 | + # that need a different default (e.g. the nightly-Lean job) pass |
| 31 | + # `default: true` so the pre-install step below flips it. |
| 32 | + - name: Install elan (Linux/macOS, if not cached) |
| 33 | + if: runner.os != 'Windows' |
| 34 | + shell: bash |
| 35 | + run: | |
| 36 | + HOME_OVERRIDE="$GITHUB_WORKSPACE/.lean4-test-home" |
| 37 | + mkdir -p "$HOME_OVERRIDE" |
| 38 | + if [ ! -x "$HOME_OVERRIDE/.elan/bin/elan" ]; then |
| 39 | + HOME="$HOME_OVERRIDE" ELAN_HOME="$HOME_OVERRIDE/.elan" \ |
| 40 | + bash vscode-lean4/scripts/elan-install/install-unix.sh |
| 41 | + fi |
| 42 | + echo "$HOME_OVERRIDE/.elan/bin" >> "$GITHUB_PATH" |
| 43 | +
|
| 44 | + - name: Install elan (Windows, if not cached) |
| 45 | + if: runner.os == 'Windows' |
| 46 | + shell: pwsh |
| 47 | + run: | |
| 48 | + $homeOverride = Join-Path $env:GITHUB_WORKSPACE '.lean4-test-home' |
| 49 | + New-Item -ItemType Directory -Force -Path $homeOverride | Out-Null |
| 50 | + $elanBin = Join-Path $homeOverride '.elan\bin\elan.exe' |
| 51 | + if (-not (Test-Path $elanBin)) { |
| 52 | + $env:USERPROFILE = $homeOverride |
| 53 | + $env:ELAN_HOME = (Join-Path $homeOverride '.elan') |
| 54 | + & "$env:GITHUB_WORKSPACE\vscode-lean4\scripts\elan-install\install-windows.ps1" |
| 55 | + if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE } |
| 56 | + } |
| 57 | + Add-Content -Path $env:GITHUB_PATH -Value (Join-Path $homeOverride '.elan\bin') |
| 58 | +
|
| 59 | + # `elan-init` only installs the elan binary and records `:stable` as the |
| 60 | + # default toolchain — it does *not* fetch the toolchain itself. Without |
| 61 | + # this step, the first test that resolves the channel eats the full |
| 62 | + # toolchain download and a network blip there surfaces as a confusing |
| 63 | + # test failure rather than a named CI step. `elan toolchain install` |
| 64 | + # eagerly re-resolves the channel, so it also covers the cache-hit / |
| 65 | + # channel-rotated case (cache restored from a previous run with an older |
| 66 | + # resolution → this step downloads the new toolchain). |
| 67 | + # |
| 68 | + # `elan toolchain install` is *not* idempotent: it errors with |
| 69 | + # `'leanprover/lean4:vX.Y.Z' is already installed` when the cache |
| 70 | + # already holds the resolved version. Treat that specific message as |
| 71 | + # success — we wanted the toolchain installed and it is — while |
| 72 | + # propagating any other non-zero exit (network failure, bad channel, |
| 73 | + # etc.). |
| 74 | + # |
| 75 | + # `shell: bash` works on Windows too because GitHub-hosted Windows |
| 76 | + # runners ship Git Bash; `elan` is the same idempotency contract on |
| 77 | + # both OSes once on PATH. |
| 78 | + - name: Pre-install ${{ inputs.channel }}${{ inputs.default == 'true' && ' + set as elan default' || '' }} |
| 79 | + shell: bash |
| 80 | + env: |
| 81 | + ELAN_HOME: ${{ github.workspace }}/.lean4-test-home/.elan |
| 82 | + CHANNEL: ${{ inputs.channel }} |
| 83 | + SET_DEFAULT: ${{ inputs.default }} |
| 84 | + run: | |
| 85 | + if out=$(elan toolchain install "$CHANNEL" 2>&1); then |
| 86 | + echo "$out" |
| 87 | + else |
| 88 | + ec=$? |
| 89 | + echo "$out" |
| 90 | + echo "$out" | grep -q 'is already installed' || exit "$ec" |
| 91 | + fi |
| 92 | + if [ "$SET_DEFAULT" = "true" ]; then |
| 93 | + elan default "$CHANNEL" |
| 94 | + fi |
0 commit comments