From 290fca4dd50caa3f1a198b44462161a9acb12621 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 15 Aug 2026 18:48:10 +0000 Subject: [PATCH] lakefile: include the library root modules in each `lean_lib` `globs := #[.submodules `X]` selects the submodules of `X` but not `X` itself, so `ZipForStd.lean` and `ZipCommon.lean` were not members of their own libraries. A shared library built from such a `lean_lib` therefore has no `initialize_` symbol, and a dependent package built with `precompileModules := true` fails to load it: error loading plugin, initializer not found 'initialize_lean_x2dzip_x2dcommon_ZipForStd' `.andSubmodules` selects the root module too. Patch authored by Claude Fable 5 (Anthropic's Claude Code). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01TK6r4jXLa2tKRNP9orsXN6 --- lakefile.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index d010ad7..bf7a128 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,13 +7,20 @@ package «lean-zip-common» where -- Both libraries are default targets, so a bare `lake build` (what CI runs) -- actually builds them. Without this Lake has nothing to do and reports -- "Build completed successfully (0 jobs)". +-- +-- `.andSubmodules`, not `.submodules`: the latter excludes the root module +-- itself, so `ZipForStd.lean`/`ZipCommon.lean` were left out of the library. +-- A shared library built from such a lib has no `initialize_` symbol, and +-- a dependent package with `precompileModules := true` then fails to load it +-- ("error loading plugin, initializer not found +-- 'initialize_lean_x2dzip_x2dcommon_ZipForStd'"). @[default_target] lean_lib ZipForStd where - globs := #[.submodules `ZipForStd] + globs := #[.andSubmodules `ZipForStd] @[default_target] lean_lib ZipCommon where - globs := #[.submodules `ZipCommon] + globs := #[.andSubmodules `ZipCommon] -- IO FFI (Handle seek/fileSize shims — no external library deps) input_file io_ffi.c where