Skip to content

chore: add trace nodes for highlighting operations #145

chore: add trace nodes for highlighting operations

chore: add trace nodes for highlighting operations #145

Workflow file for this run

on:
push:
pull_request:
name: CI
jobs:
build:
strategy:
matrix:
toolchain:
- "4.3.0"
- "4.4.0"
- "4.5.0"
- "4.6.0"
- "4.7.0"
- "4.8.0"
- "4.9.0-rc1"
- "nightly-2024-06-12"
platform:
- os: ubuntu-latest
installer: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
# Mac runners are rare and expensive, so spot-check that the
# subprocess support seems OK but be less thorough
include:
- toolchain: "4.8.0"
platform:
os: macos-latest
installer: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
- toolchain: "4.8.0"
platform:
os: macos-latest
installer: |
brew install elan-init
- toolchain: "4.3.0"
platform:
os: macos-latest
installer: |
brew install elan-init
name: Build and test (${{ matrix.platform.os }}, ${{ matrix.platform.installer}}, ${{ matrix.toolchain}})
runs-on: ${{ matrix.platform.os }}
steps:
- name: Install elan
run: |
set -o pipefail
${{ matrix.platform.installer }}
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Which lake?
run: |
which lake
- uses: actions/checkout@v3
- name: List all files
run: |
find . -name "*.lean" -type f
- name: Select Lean version
run: |
echo "leanprover/lean4:${{ matrix.toolchain }}" > lean-toolchain
- name: Lean version
run: |
lean --version
- name: Cache .lake
uses: actions/cache@v3
with:
path: .lake
key: ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}
- name: Build the project
run: |
lake build
- name: Configure demo/test subproject
run: |
pushd demo
lake update
lake build :examples
popd
- name: Run tests
run: |
lake exe subverso-tests