SilverSight/.github/workflows/q16-roundtrip.yml

16 lines
758 B
YAML

name: Q16_16 Roundtrip
on: [push, pull_request]
jobs:
roundtrip:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Build C library
run: gcc -shared -fPIC -O2 -o c/libq16.so c/q16_canonical.c
- name: Build and run roundtrip
run: |
lake build q16-roundtrip
lake exe q16-roundtrip 2>/dev/null | python3 -c 'import json,sys; d=json.load(sys.stdin); assert d["ok"], f"{d[\"failed\"]} failures"; print(f"OK: {d[\"passed\"]}/{d[\"total\"]} passed (0 failed)")'
- name: Verify C/Lean agreement
run: |
lake exe q16-roundtrip 2>/dev/null | python3 -c 'import json,sys; d=json.load(sys.stdin); print(f"C/Lean roundtrip: {d[\"passed\"]}/{d[\"total\"]} consistent")'