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"