Skip to content

feat: Rounding Proof: Galois Connection [3/?] #85

feat: Rounding Proof: Galois Connection [3/?]

feat: Rounding Proof: Galois Connection [3/?] #85

Workflow file for this run

name: Unit Tests
on:
push:
branches:
- main
pull_request:
merge_group:
permissions:
contents: read
jobs:
unit-tests:
name: SMT-LIB Relation Tests
runs-on: ubuntu-latest
steps:
- name: Checkout 🛎️
uses: actions/checkout@v4
- name: Build with lean-action
uses: leanprover/lean-action@v1
with:
use-mathlib-cache: false
use-github-cache: true
build: true
test: false
- name: Run FpMaxRel test
run: ./.lake/build/bin/fp-lean fpMaxRel
- name: Run FpMinRel test
run: ./.lake/build/bin/fp-lean fpMinRel
- name: Run FpLtRel test
run: ./.lake/build/bin/fp-lean fpLtRel
- name: Run FpIeeeEqRel test
run: ./.lake/build/bin/fp-lean fpIeeeEqRel
- name: Run Rational Add test (xfail)
run: ./.lake/build/bin/fp-lean addRat --xfail
- name: Run Rational Mul test
run: ./.lake/build/bin/fp-lean mulRat
- name: Run Rational Div test (xfail)
run: ./.lake/build/bin/fp-lean divRat --xfail