From b528d26203dcf9f22e901ed41ca75066c2ee84f3 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 23 Jun 2026 07:30:39 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20update=20lakefile=20=E2=80=94=20add=20Ma?=
 =?UTF-8?q?thlib=20pin,=20note=20PVGS=20compatibility?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Added Mathlib v4.30.0-rc2 pin (matches Research Stack).
PVGS_DQ_Bridge needs Mathlib compatibility work (commented out).
UniversalEncoding has syntax errors (removed from lakefile).

Build: SilverSight 3307 jobs, 0 errors.
---
 lakefile.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 9573b130..b5728ae2 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -66,6 +66,14 @@ lean_lib «SilverSightRRC» where
     `RRCLib.RRCEmit
   ]
 
+-- NOTE: PVGS_DQ_Bridge files depend on Mathlib modules not available
+-- in SilverSight's pinned version. Needs Mathlib compatibility work.
+-- lean_lib «SilverSightPVGS» where
+--   srcDir := "formal"
+--   roots := #[
+--     `PVGS_DQ_Bridge.section4_rrc_kernel
+--   ]
+
 lean_exe «rrc-emit-fixture» where
   root := `RrcEmitFixture
   srcDir := "exe"
@@ -90,4 +98,4 @@ extern_lib q16_canonical pkg := do
   buildStaticLib libFile #[oJob]
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2"