Skip to content

Commit

Permalink
feat: add Windows runner support (#99)
Browse files Browse the repository at this point in the history
Change `${{ github.action_path }}` to `${GITHUB_ACTION_PATH}` to add
support for Windows runners

Add a functional test on a Windows runner

Closes #75
  • Loading branch information
austinletson authored Sep 6, 2024
1 parent f8a2d35 commit 8fc2853
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 13 deletions.
13 changes: 11 additions & 2 deletions .github/workflows/functional_tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ jobs:
- uses: ./.github/functional_tests/auto_config_false
with:
toolchain: ${{ env.toolchain }}

detect-mathlib:
runs-on: ubuntu-latest
steps:
Expand Down Expand Up @@ -117,7 +117,7 @@ jobs:
- uses: ./.github/functional_tests/subdirectory_lake_package
with:
toolchain: ${{ env.toolchain }}

macos-runner:
runs-on: macos-latest
steps:
Expand All @@ -127,3 +127,12 @@ jobs:
lake-init-arguments: "standalone"
toolchain: ${{ env.toolchain }}

windows-runner:
runs-on: windows-latest
steps:
- uses: actions/checkout@v4
- uses: ./.github/functional_tests/lake_init_success
with:
lake-init-arguments: "standalone"
toolchain: ${{ env.toolchain }}

4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## Unreleased

### Added

- Windows GitHub runner support

### Fixed

- replace `actions/cache` with `actions/cache/restore` to prevent redundant cache saving
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@ jobs:
```
> [!IMPORTANT]
`lean-action` is tested on `ubuntu-latest` and `macos-latest` GitHub-hosted runners,
and should support Unix-based runners in general.
Currently, `lean-action` does not support Windows runners.
`lean-action` is tested on `ubuntu-latest`, `macos-latest`, and `windows-latest` GitHub-hosted runners.
We recommend using one of these runners for the best experience,
however if you encounter an issue when using a different runner, please still open an issue.

## Configuring which features `lean-action` runs

Expand Down
16 changes: 8 additions & 8 deletions action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ runs:
- name: install elan
run: |
: Install Elan
${{ github.action_path }}/scripts/install_elan.sh
${GITHUB_ACTION_PATH}/scripts/install_elan.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -125,7 +125,7 @@ runs:
LINT: ${{ inputs.lint }}
run: |
: Configure Lean Action
${{ github.action_path }}/scripts/config.sh
${GITHUB_ACTION_PATH}/scripts/config.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -143,7 +143,7 @@ runs:
id: detect-mathlib
run: |
: Detect Mathlib
${{ github.action_path }}/scripts/detect_mathlib.sh
${GITHUB_ACTION_PATH}/scripts/detect_mathlib.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -166,7 +166,7 @@ runs:
BUILD_ARGS: ${{ inputs.build-args }}
run: |
: Lake Build
${{ github.action_path }}/scripts/lake_build.sh
${GITHUB_ACTION_PATH}/scripts/lake_build.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -181,7 +181,7 @@ runs:
if: ${{ steps.config.outputs.run-lake-test == 'true'}}
run: |
: Lake Test
${{ github.action_path }}/scripts/lake_test.sh
${GITHUB_ACTION_PATH}/scripts/lake_test.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -191,7 +191,7 @@ runs:
if: ${{ steps.config.outputs.run-lake-lint == 'true'}}
run: |
: Lake Lint
${{ github.action_path }}/scripts/lake_lint.sh
${GITHUB_ACTION_PATH}/scripts/lake_lint.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

Expand All @@ -200,7 +200,7 @@ runs:
# Passes in the private status, number of stars, and license id of the repository to check_reservoir_eligibility.sh script
run: |
: Check Reservoir Eligibility
${{ github.action_path }}/scripts/check_reservoir_eligibility.sh \
${GITHUB_ACTION_PATH}/scripts/check_reservoir_eligibility.sh \
"${{ github.event.repository.private }}"\
"${{ github.event.repository.stargazers_count }}"\
"${{ github.event.repository.license.spdx_id }}"
Expand All @@ -211,6 +211,6 @@ runs:
if: ${{ inputs.lean4checker == 'true' }}
run: |
: Check Environment with lean4checker
${{ github.action_path }}/scripts/run_lean4checker.sh
${GITHUB_ACTION_PATH}/scripts/run_lean4checker.sh
shell: bash
working-directory: ${{ inputs.lake-package-directory }}

0 comments on commit 8fc2853

Please sign in to comment.