Skip to content

chore: more informative tests for debugging #36

chore: more informative tests for debugging

chore: more informative tests for debugging #36

Workflow file for this run

on:
push:
pull_request:
name: Continuous Integration
jobs:
build:
strategy:
matrix:
toolchain:
- "leanprover/lean4:4.3.0"
- "leanprover/lean4:4.4.0"
- "leanprover/lean4:4.5.0"
- "leanprover/lean4:4.6.0"
name: Build and test
runs-on: ubuntu-latest
steps:
- name: Install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
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 "${{ 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
~/.elan/bin/lake update
~/.elan/bin/lake build :examples
popd
- name: Run tests
run: |
lake exe subverso-tests