CI #413
Workflow file for this run
This file contains hidden or 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
| # SPDX-License-Identifier: MPL-2.0 | |
| # This workflow is managed by gh actions-lock. | |
| name: CI | |
| on: | |
| push: | |
| branches: [main, master, 'claude/**'] | |
| pull_request: | |
| branches: [main, master] | |
| permissions: | |
| contents: read | |
| jobs: | |
| test: | |
| name: Idris2 core tests | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Install Idris2 0.8.0 | |
| env: | |
| # Exact commit referenced by the upstream v0.8.0 tag. | |
| IDRIS2_REVISION: 15a3e4e70843f7a34100f6470c04b791330788df | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update -qq | |
| if sudo apt-get install -y idris2; then | |
| idris2 --version | |
| else | |
| sudo apt-get install -y chezscheme make libgmp-dev | |
| git clone --filter=blob:none --no-checkout \ | |
| https://github.com/idris-lang/Idris2.git /tmp/idris2 | |
| git -C /tmp/idris2 checkout --detach "$IDRIS2_REVISION" | |
| make -C /tmp/idris2 bootstrap SCHEME=scheme | |
| make -C /tmp/idris2 install PREFIX="$HOME/.idris2" | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| "$HOME/.idris2/bin/idris2" --version | |
| fi | |
| - name: Build and run core tests | |
| run: | | |
| set -euo pipefail | |
| idris2_prefix="$(dirname "$(dirname "$(command -v idris2)")")" | |
| export IDRIS2_PREFIX="$idris2_prefix" | |
| idris2 --build ubicity-tests.ipkg | |
| ./build/exec/ubicity-tests |