From 140825c54f259caddc5b3d9131da1f81d8ad3d80 Mon Sep 17 00:00:00 2001 From: Lars Kuhtz Date: Tue, 11 Aug 2026 12:21:46 -0700 Subject: [PATCH] Disable unbuildable case-study libraries on the Veil-support branch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This branch upgrades only the Loom core needed by Veil (37fe563); the case studies were not ported and still import Loom.MonadAlgebras.NonDetT.Extract, which was dropped — so the CaseStudiesBase/Cashmere/Velvet/CaseStudies libraries cannot build at any revision of this branch. Because the CaseStudies lib's globs also overlap the core library, consumers that precompile modules (Veil with precompileModules := true) get CaseStudies:shared pulled into their build and fail on the missing module. Comment the four case-study libs out and switch the Loom lib to Glob.andSubmodules so the root Loom module is covered by the library. Co-Authored-By: Claude Fable 5 --- lakefile.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index a7093b8..75ba322 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -115,10 +115,21 @@ def CaseStudiesRoot : Array Glob := @[default_target] lean_lib Loom { - globs := #[Glob.submodules `Loom] + -- `andSubmodules`: cover the root `Loom` module as well, so consumers + -- importing `Loom` resolve it to this library. + globs := #[Glob.andSubmodules `Loom] extraDepTargets := #[``downloadDependencies] } +/- The case-study libraries are disabled on this branch: it upgrades only +the Loom core needed by Veil (see 37fe563), and the case studies were not +ported — `CaseStudies/*` still imports `Loom.MonadAlgebras.NonDetT.Extract`, +which no longer exists here, so these libraries cannot build. Worse, the +`CaseStudies` lib's globs overlap the core (`Glob.submodules `Loom`), so a +consumer that precompiles (e.g. Veil with `precompileModules`) gets +`CaseStudies:shared` pulled into its build and fails on the missing module. +The case studies live on `master`. + lean_lib CaseStudiesBase { globs := CaseStudiesRoot } @@ -134,3 +145,4 @@ lean_lib Velvet { lean_lib CaseStudies { globs := #[Glob.submodules `Loom, Glob.submodules `CaseStudies] } +-/