Zulip Chat Archive

Stream: lean4

Topic: Plugin: Nondeterministic "offset 0" on building shared facet

Thomas Murrills (Dec 17 2025 at 21:19):

When building a shared library and linking a dependency of that shared library statically via moreLinkObjs = ["pkg/tgt:static"] (as in #lean4 > Load plugin during build?), sometimes I see a

⚠ [710/765] Built Batteries.Data.Char.Basic:c.o
warning: /Users/thomas/LeanContribution/thorimur/mathlib4/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Char/Basic.c.o.export.trace: offset 0: unexpected end of input

and this seems to break things when using the shared library as a plugin later (by emitting a similar "offset 0" error). But sometimes, it builds without issue.

However, I tried minimizing, and have been unsuccessful. :( This only seems to happen on the branch I'm using for experimenting with making Mathlib.Init a plugin, which you can find at #33015 (draft PR created only for convenient sharing).

(Note for the concerned reader: I have zero plans to actually make Mathlib.Init a plugin—it's just a really useful test case for exploring plugins due to its complexity and convenient "separation" from Mathlib! :) )

To be clear, what I'm running here is lake build MathlibInit. You can see a log demonstrating the nondeterminism here (the second lake build MathlibInit is successful, but the third has different errors!)

shell log

And for reference, here's an example of the similar error I see upon lake build Mathlib sometimes:

lake build Mathlib error

(This occurs for many different files referencing files in MathlibInit.)

Last updated: Dec 20 2025 at 21:32 UTC