Closed Seasawher closed 4 weeks ago
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?
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.
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.
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
.
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...)