install elan on windows

[Seasawher]

I have created a workflow running on Windows.

see: https://github.com/lean-ja/lean-by-example/blob/edc6f5e9d023b0f4c4beb26474e1b678b8e9ba5e/.github/workflows/ci.yml#L29

Almost always building on Windows is not necessary, but I sometimes need this. (For example, when trying to provide an environment which reproduce a lean bug on Windows machine...)

[Seasawher]

I think there should be a conditional branch that detects the runner OS and installs elan in a different way if it is Windows. How do you think?

[austinletson]

It would be possible to use conditional logic to achieve this, however, I think it would require rewriting most of the scripts that power most of the functionality of lean-action for a Windows environment since they are written in Bash.

I know some GitHub actions support multiple runner operating systems by writing the action in TypeScript instead of having shell scripts and then using shell scripts for specific OS-specific components, e.g., setup-PHP. There are other advantages to using TypeScript instead of the current lean-action architecture so this could be a worthwhile refactor in the future.

[joneugster]

My Windows workflow currently reads:

- name: Install elan (Windows)
  if: matrix.os == 'windows-latest'
  run: |
    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
    bash elan-init.sh -y
    echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH
  shell: bash
- name: Run lake build (Windows)
  if: matrix.os == 'windows-latest'
  run: |
    cd your/local/folder
    lake build
  shell: bash

Thought I'd post it here for reference as it's using bash instead of powershell which is closer to the existing scripts of the lean action.

[austinletson]

Thank you for the tip here @joneugster!

I have a PR open to add support for Windows runners. We can use the existing scripts with a slight modification to the call site because of a known issue with GitHub custom actions (link to issue).

Windows runner support should be available in the next week or two with the next release of lean-action.