Skip to content

defined and proved bbT #279

defined and proved bbT

defined and proved bbT #279

Workflow file for this run

name: CI
on: [push, pull_request, workflow_dispatch]
jobs:
build:
name: ${{ matrix.name }}
runs-on: ${{ matrix.os }}
strategy:
matrix:
include:
- name: Linux
os: ubuntu-latest
steps:
- name: Install Elan (Linux)
if: matrix.os == 'ubuntu-latest'
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Install cvc5 (Linux)
if: matrix.os == 'ubuntu-latest'
run: |
mkdir -p "$HOME/.local/bin"
curl https://github.com/HanielB/cvc5/releases/download/leanPrinter-v0.0.4/cvc5-Linux-2023-03-10-f9e30de2dd -L > "$HOME/.local/bin/cvc5"
chmod +x "$HOME/.local/bin/cvc5"
echo "$HOME/.local/bin" >> $GITHUB_PATH
- name: Checkout
uses: actions/checkout@v2
- name: Build lean-smt
run: |
lake update
lake exe cache get
lake build +Smt:dynlib
- name: Test lean-smt
run: lake run test