fixes for leanprover/lean4#5749 #347
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
on: | |
push: | |
pull_request: | |
name: ci | |
jobs: | |
build: | |
name: ${{ matrix.name }} | |
runs-on: ${{ matrix.os }} | |
defaults: | |
run: | |
shell: ${{ matrix.shell || 'sh' }} | |
strategy: | |
matrix: | |
include: | |
- name: Build on Ubuntu | |
os: ubuntu-latest | |
# TODO: investigate why `lake build` deadlocks on macOS (issue #33) | |
#- name: Build on macOS | |
# os: macos-latest | |
- name: Build on Windows | |
os: windows-latest | |
shell: msys2 {0} | |
steps: | |
- name: Install MSYS2 (Windows) | |
if: matrix.os == 'windows-latest' | |
uses: msys2/setup-msys2@v2 | |
with: | |
path-type: inherit | |
install: curl unzip | |
- name: Install elan | |
shell: bash | |
run: | | |
curl -sSfLO https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | |
chmod +x elan-init.sh | |
./elan-init.sh -y --default-toolchain none | |
echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
- uses: actions/checkout@v4 | |
- name: Update NPM (Windows) | |
shell: bash | |
if: matrix.os == 'windows-latest' | |
# See https://github.com/nodejs/node/issues/52682 | |
run: cd widget/ && npm install npm | |
- name: Build package | |
run: lake build ProofWidgets | |
- name: Build demos | |
run: lake build ProofWidgets.Demos | |
- name: Create GitHub release for tag (Ubuntu) | |
if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest' | |
uses: softprops/action-gh-release@v1 | |
- name: Upload release archive (Ubuntu) | |
if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest' | |
run: lake upload $RELEASE_TAG | |
env: | |
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
RELEASE_TAG: ${{ github.ref_name }} | |
- name: Test release archive (Ubuntu) | |
if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest' | |
run: lake clean && lake build :release && lake build --no-build |