This repository has been archived by the owner on Aug 24, 2024. It is now read-only.
fix: print-paths changed to setup-file in Lean v4.4.0
#215
Workflow file for this run
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
| name: CI | |
| on: | |
| push: | |
| branches: [ main ] | |
| pull_request: | |
| branches: [ main ] | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| name: ${{ matrix.name }} | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: ${{ matrix.shell || 'sh' }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: Ubuntu | |
| os: ubuntu-latest | |
| - name: macOS | |
| os: macos-latest | |
| - name: Windows | |
| os: windows-latest | |
| shell: pwsh | |
| steps: | |
| # Fix CR/LF mangling on Windows | |
| - name: Disable autocrlf in git | |
| run: git config --global core.autocrlf false | |
| # Checkout repository | |
| - uses: actions/checkout@v2 | |
| # Install elan with nightly toolchain | |
| - name: Install Elan (macOS) | |
| if: matrix.os == 'macos-latest' | |
| run: | | |
| set -o pipefail | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install Elan (Ubuntu) | |
| if: matrix.os == 'ubuntu-latest' | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install Elan (Windows) | |
| if: matrix.os == 'windows-latest' | |
| run: | | |
| curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | |
| .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain none | |
| echo "$HOME\.elan\bin" >> $env:GITHUB_PATH | |
| # Build and test | |
| - name: Build LeanInk | |
| run: lake build | |
| # Upload artifact | |
| - name: Upload artifacts | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ matrix.os }} | |
| path: build | |
| - name: Run tests | |
| run: lake script run tests |