From 8fd46382405bd50eee0321119307ecbf2036bfac Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 23 Jun 2026 05:56:27 -0500 Subject: [PATCH] fix: eliminate cross-project Semantics.FixedPoint imports Schema.lean and Receipt.lean now import SilverSight.FixedPoint instead of Semantics.FixedPoint. SilverSight builds standalone. Build: 3307 jobs, 0 errors. --- formal/SilverSight/Receipt.lean | 6 +++--- formal/SilverSight/Schema.lean | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/formal/SilverSight/Receipt.lean b/formal/SilverSight/Receipt.lean index f5a07e8d..a7700ea2 100644 --- a/formal/SilverSight/Receipt.lean +++ b/formal/SilverSight/Receipt.lean @@ -1,9 +1,9 @@ -import Semantics.FixedPoint +import SilverSight.FixedPoint namespace SilverSight -open Semantics.FixedPoint -open Semantics.FixedPoint.Q16_16 +open SilverSight.FixedPoint +open SilverSight.FixedPoint.Q16_16 -- ═══════════════════════════════════════════════════════════════════════════ -- §1 Gate types diff --git a/formal/SilverSight/Schema.lean b/formal/SilverSight/Schema.lean index c9594db3..06bd3462 100644 --- a/formal/SilverSight/Schema.lean +++ b/formal/SilverSight/Schema.lean @@ -1,8 +1,8 @@ -import Semantics.FixedPoint +import SilverSight.FixedPoint namespace SilverSight -open Semantics.FixedPoint +open SilverSight.FixedPoint /-- A Schema describes the wire-level layout of a type: - `byteSize`: the number of bytes in the wire representation