fix: lake: fetch plugin and link facets on the fetching thread

[rbeauchamp]

This PR makes Lake fetch a library's or module's shared library, static library or object file named by key in plugins, dynlibs, moreLinkObjs or moreLinkLibs, such as Plug:shared, directly rather than in a job continuation when it prepares a module for elaboration or links an executable or a module's shared library. Previously, the modules of a library with plugins = ["Plug:shared"] could each start a job for Plug:shared, and the duplicate jobs could overwrite each other's outputs and fail the build.

PartialBuildKey.fetchIn fetches a facet in a bindM continuation of its target's job. Continuations run on worker threads alongside other fetches, and the build store looks a key up and stores its job in separate steps, so two continuations could both miss the key and both create its job. The new internal Target.fetchInBlocking and TargetArray.fetchInBlocking bind the fetch synchronously, so that it runs before they return, with the continuation's cancellation check, failure handling and data kind, when the facet is one of Lake's own library facets shared, static and static.export or module facets dynlib, o, c.o and bc.o (with their variants), and the job of its target has finished, as the job of a module, a package or a configured target always has. Otherwise they bind it as fetchIn does. They are used only where Lake fetches these keys after waiting for a module's imports: in Module.recFetchPreSetup, recComputeModuleLinkInfo, Module.recBuildDynlib, setupEditedModule and setupExternalModule.

The facet's fetch function now runs in place, and with it every fetch function that it calls in place, and they can block, as Module.recFetchPreSetup can since #13601 when it awaits needs. For Plug:shared, they include the presetup of each of Plug's modules, which awaits Plug's needs, and the fetch functions of the custom targets and extern_libs that Plug links. The waits before the fetch return at once when the jobs they wait for have finished. So code that fetches a module's presetup, dynlib or link information from a (sync := true) task, which did not block there before, can now block, and Task.get panics in such a task. If one of those jobs or fetch functions waits for something that the fetching code does only after the fetch returns, such as resolving a promise, the build now hangs.

Other fetches are unchanged. A package's own facets (e.g., from library_facet), the facets of an extern_lib, and a facet whose target's job is still running, such as a facet of a custom target, are still fetched in a continuation and can still start duplicate jobs. So are a library's needs (LeanLib.recBuildExtraDepTargets) and the moreLinkObjs and moreLinkLibs of its static and shared facets, which are fetched in functions with no earlier wait on every path. Naming a default facet by its target alone, e.g., needs = ["a"] for a:exe, avoids this, since Lake fetches a target's default facet in place. PartialBuildKey.fetchIn, BuildKey.fetch and Target.fetchIn behave as before, as do the continuation fetches of Module.computeExportInfo, Module.computeMetaExportInfo and Module.recBuildIRArts, which find stored keys under Lake's builtin facets. Code in a package that fetches a key not yet stored from its own job continuation, e.g., in Job.async or Job.mapM, can also still race in the same way.

AI assistance: Claude Opus 5.5 in Claude Code contributed to the fix, the tests and this description, and GPT-6.1 Sol (OpenAI) reviewed the change. I have reviewed the changes.

Part of #15435

[rbeauchamp]

Notes for review:

• Where fetchInBlocking is used. Each call follows a wait for a module's imports on every path: Module.recFetchPreSetup (src/lake/Lake/Build/Module.lean:649-650) awaits its library's extraDep (:627) and its imports (:643); recComputeModuleLinkInfo (:1498-1506) waits for the root's transitive imports (:1492); Module.recBuildDynlib (:1548) awaits the module's imports (:1545); setupEditedModule (:1636-1637) and setupExternalModule (:1679-1680) await the file's imports (:1629, :1631, :1675) and run only as the top-level build, in a pool task (src/lake/Lake/Build/Run.lean:392).
• What can newly block or hang, and a question. fetchInBlocking fetches in place only Lake's own link facets (src/lake/Lake/Build/Target/Fetch.lean:23-26) of a target whose job has finished (:76-77); it never waits for that job. The waits before it return at once when their jobs have finished, so they do not show that the caller may block. The facet's fetch function then runs in place, with the fetch functions that it calls in place: for Plug:shared, LeanLib.recBuildShared (src/lake/Lake/Build/Library.lean:139) waits on import parsing (:54); it fetches each module's object file (:143), whose fetch functions reach the module's presetup (src/lake/Lake/Build/Module.lean:1423, :1377, :1302, :1142), which awaits the library's needs (:626-627); and it fetches the custom targets and extern_libs that the library links (Library.lean:144-145, :158-161; src/lake/Lake/Build/ExternLib.lean:25). So, first, if code fetches a module's presetup from a (sync := true) continuation after the module's imports and needs have finished, recFetchPreSetup did not block before this PR and now can, and Task.get panics there (src/runtime/object.cpp:1028). Second, if one of those jobs or fetch functions waits for something that the code fetching the presetup does only after the fetch returns, such as resolving a promise, the build now hangs. The same holds for a module's dynlib and link information. The first is the exposure fix: lake: await needs before processing module headers #13601 accepted for needs. The alternative is a fix in the build store that lets concurrent fetches of a key share one job without moving any fetch; my attempts at that ran into other costs (a second fetch has to wait for the first or get a placeholder job, and cycles that span threads are then not reported). Would you prefer that direction, or this one?
• Facets still fetched in a continuation. A package's own facet runs the package's fetch function, which can wait for anything: in the test, the facet gated waits for a promise that gatedFetched resolves only after its fetch of a module's presetup returns, so fetching it in place would hang where fetchIn does not. An extern_lib's facets run the fetch function of its own target at once (ExternLib.lean:25). A custom target's job, or a facet's output, can still be running (src/lake/Lake/Build/Index.lean:35), and waiting for it can hang in the same way (delayed in the test); the jobs of modules, packages and configured targets have always finished (Index.lean:38, Target/Fetch.lean:33-44). These facets keep the continuation and can still start duplicate jobs. The list is matched by name, and a package's facet declaration replaces Lake's of the same name (src/lake/Lake/Load/Workspace.lean:39, src/lake/Lake/Load/Resolve.lean:50), so a package that does that has its own fetch function run in place.
• Where it is not used. LeanLib.recBuildExtraDepTargets (src/lake/Lake/Build/Library.lean:180, the needs of a library or an executable) has no wait before its fetches. LeanLib.recBuildStatic (:101) and LeanLib.recBuildShared (:145, :159) have none on every path: their fetch of the library's modules waits on import parsing (:54) only while the modules have not been collected and the library has some. needs is the case in Lake: facet keys in needs can create duplicate build jobs #15435, so this PR does not close it. fetchInBlocking would fix it in recBuildExtraDepTargets, with the same kind of exposure as above: Lake fetches a library's extraDep only in recFetchPreSetup, which awaits it at once (Module.lean:626-627), and in setupEditedModule, and recBuildExtraDepTargets already fetches the default facet of a needs entry without a facet in place (src/lake/Lake/Build/Target/Fetch.lean:54-58), which can block (for an executable, in recComputeModuleLinkInfo). I can add it if you want it.
• Fetches from a package's own job continuations. Code in a configuration can fetch inside Job.async, Job.mapM or Job.bindM, or inside the build functions it passes to Package.afterBuildCacheAsync, Package.afterBuildCacheSync or buildFileAfterDep. Those fetches run on worker threads and can race as before. Lake could refuse them at run time: Job.mapM, Job.bindM and Job.async would mark the continuations they run, and a fetch from a marked continuation that misses the build store would fail with an error naming the key. That breaks configurations that create keys in continuations, and the build's own top-level Job.async (src/lake/Lake/Build/Run.lean:392) would need an exemption, so I left it out.
• The returned job. fetchInBlocking keeps the bindM of fetchIn, with sync := true when IO.hasFinished says the target's job has finished, and a sync bind on a finished task runs its continuation before returning (lean_task_bind_core, src/runtime/object.cpp:1270-1271). So the cancellation check, a failed or canceled target job, and the data kind of the facet's job are handled as before. A later fetch finds the stored job only for a memoized facet whose fetch function returned a job, a failed one included; a facet with memoize := false, such as o, runs its fetch function on every fetch, as before (src/lake/Lake/Build/Index.lean:49-50), and stores only the keys that it fetches.
• Unchanged continuation fetches. Module.computeExportInfo, Module.computeMetaExportInfo and Module.recBuildIRArts fetch their own module's input, importInfo and presetup inside continuations. With Lake's builtin facets those keys are already stored when the continuations run, so they are left as they are.
• Tests. pluginsFetched and linkLibsFetched fetch the presetup and dynlib of a module whose library names Lib:shared in plugins or moreLinkLibs, and fail unless the build store has a job for Lib:shared by then. They run with LEAN_NUM_THREADS=1. The build's top-level fetch holds the only worker, a non-sync bindM continuation is queued even when the target's job has finished (lean_task_bind_core), and nothing after the fetch of the key waits on a task, so before this PR the key was not stored yet on any schedule. gatedFetched and delayedFetched fetch the presetup of a module whose plugin waits for a promise, in the fetch function of a package's own facet or in the job of a custom target, and only then resolve the promise; they terminate only if fetchInBlocking leaves those facets to a continuation.
• Cost. The facet's fetch function now runs in the calling fetch function, so its waits block that thread; in a pool task, the task manager adds a worker meanwhile (task_manager::wait_for). I have not measured the effect on build times.