From 2a45da046201ca87c890b5bc2548e6bb66024e77 Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 27 Jun 2026 23:14:36 -0500 Subject: [PATCH] fix(build): register missing CoreFormalism roots in lakefile Registered CoreFormalism.HachimojiManifoldAxiom and CoreFormalism.ChentsovFinite to library roots to resolve build/import issues for downstream RRC files. Build: 3343 jobs, 0 errors (lake build) --- lakefile.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lakefile.lean b/lakefile.lean index e4c0d81e..38cbf85a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -37,6 +37,8 @@ lean_lib «SilverSightFormal» where `CoreFormalism.HachimojiCodec, `CoreFormalism.HachimojiLUT, `CoreFormalism.HachimojiBridging, + `CoreFormalism.HachimojiManifoldAxiom, + `CoreFormalism.ChentsovFinite, `SilverSight.WireFormat, `SilverSight.ProductSchema, `SilverSight.ProductWireFormat,