mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
28 lines
1 KiB
YAML
28 lines
1 KiB
YAML
name: Lean Check
|
|
on: [push, pull_request]
|
|
jobs:
|
|
build:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
- name: Install Lean
|
|
uses: leanprover/lean-action@v1
|
|
- name: Build default target
|
|
run: lake build
|
|
- name: Build formal library
|
|
run: lake build SilverSightFormal
|
|
- name: Check for non-TODO sorries
|
|
run: |
|
|
SORRY_COUNT=$(grep -rn "^ sorry$\|^ sorry$\|^sorry$" formal/SilverSight/ Core/ || true | wc -l)
|
|
if [ "$SORRY_COUNT" -gt 0 ]; then
|
|
echo "WARNING: Found $SORRY_COUNT non-TODO sorries"
|
|
fi
|
|
echo "OK: $(grep -rn 'TODO(lean-port)' formal/ --include='*.lean' || true | wc -l) TODO(lean-port) markers known"
|
|
- name: Check for admit
|
|
run: |
|
|
ADMIT_COUNT=$(grep -rn "^ admit$\|^admit$" formal/SilverSight/ Core/ || true | wc -l)
|
|
if [ "$ADMIT_COUNT" -gt 0 ]; then
|
|
echo "ERROR: Found $ADMIT_COUNT admit markers"
|
|
exit 1
|
|
fi
|
|
echo "No bare admits"
|