Confusing failure when failing to install elan

[Ruben-VandeVelde]

When installing elan fails, e.g. with the following output:

  info: downloading installer
  curl: (22) The requested URL returned error: 503
  elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz
  /home/runner/work/_actions/leanprover/lean-action/434f25c2f80ded67bba02502ad3a86f25db50709/scripts/install_elan.sh: line 12: /home/runner/.elan/bin/lean: No such file or directory
  /home/runner/work/_actions/leanprover/lean-action/434f25c2f80ded67bba02502ad3a86f25db50709/scripts/install_elan.sh: line 13: /home/runner/.elan/bin/lake: No such file or directory

the "Configure Lean" step succeeds, but then you get a lake: command not found error later.

Link to workflow where bug was encountered: https://github.com/leanprover-community/mathlib4/actions/runs/20139028856/job/57803536341

Details

• lean-action version: v1.3.0
• GitHub runner: ubuntu-24.04

[austinletson]

Thanks for reporting this bug!

I have submitted #143 which should fix this issue moving forward. The root cause was that scripts/install_elan.sh was missing set -e, causing the script to return success even when elan installation failed. With the fix, lean-action will now fail immediately when elan installation fails (e.g., due to transient 503 errors), making the failure clear rather than causing confusing downstream errors.