From 572a19aef6e63d18380d866c2a9ff04033dae29f Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 30 Jun 2026 06:38:04 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20Q16=20roundtrip=20CI=20=E2=80=94=20build?=
 =?UTF-8?q?=20C=20lib=20via=20lake,=20run=20executable?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/q16-roundtrip.yml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/q16-roundtrip.yml b/.github/workflows/q16-roundtrip.yml
index 02726fad..5aaba543 100644
--- a/.github/workflows/q16-roundtrip.yml
+++ b/.github/workflows/q16-roundtrip.yml
@@ -6,6 +6,11 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - name: Build C library
-        run: make -f CBridge/Makefile
-      - name: Run roundtrip test
-        run: python3 Tests/q16_roundtrip_test.py
\ No newline at end of file
+        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")'