Lake: `Module.computeExportInfo` awaits inside a `(sync := true)` continuation (incomplete fix for #13598)

Prerequisites

• Check that your issue is not already filed: this is the unfixed remainder of #13598.
• Reduce the issue to a minimal, self-contained, reproducible test case — the panic is a thread race at build scale. The defect is visible by inspection; see below.

Description

Lake.Module.computeExportInfo awaits two jobs from inside a mapM (sync := true) continuation. sync := true runs
the continuation on the thread that completed the dependency, and the runtime forbids Task.get there
(src/runtime/object.cpp:1001). When input or importInfo is still pending, the build prints:

`Task.get` called from a `(sync := true)` task

src/lake/Lake/Build/Module.lean:477-480, current master (23393b95):

def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportInfo) := do
  (← mod.leanArts.fetch).mapM (sync := true) fun arts => do
    let input ← (← mod.input.fetch).await
    let importInfo ← (← mod.importInfo.fetch).await
    ...

Context

This is the site in #13598's backtrace (frame 6, Lake.Module.computeExportInfo). PR #13601 closed #13598 by awaiting
needs targets before header processing, which removed the source of pendency in that reporter's setup — but the awaits
inside the (sync := true) continuation were not moved, so any other cause of a pending input/importInfo reproduces
the panic. Filing separately rather than reopening, since the reproduction conditions differ.

Steps to Reproduce

Nondeterministic. In a Mathlib-scale workspace (a project depending on Mathlib with its own tool executables), perturb a
tool library's module set — add or remove one module file — then run lake exe <tool>. Observed in 2 of 3 runs:

`Task.get` called from a `(sync := true)` task
backtrace:
0   libleanshared.dylib   lean::print_backtrace(bool) + 60
1   libleanshared.dylib   lean::lean_panic_impl(char const*, unsigned long, bool) + 176
2   libleanshared.dylib   lean::task_manager::wait_for(lean_task*) + 152

Expected behavior: no panic.

Actual behavior: the panic prints, and the wait then completes — so nothing is corrupted, but every affected build
emits a runtime backtrace into its output.

Additional Information

Suggested fix: fetch and await input and importInfo before entering mapM (sync := true), so the continuation
itself never blocks.

Versions

Observed on Lean/Lake 4.33.0-rc1 (62eed1db4d67327ec8120be05f1a1b0847d74561), arm64-apple-darwin. Code path unchanged
on master as of 2026-07-31 (23393b95).

Impact

Add 👍 to
issues you consider important.
If others are impacted by this issue, please ask them to add 👍 to it.

Start by inspecting src/lake/Lake/Build/Module.lean:477-480 and the Task.get restriction in src/runtime/object.cpp:1001. Reproduce with lake exe in a Mathlib-scale workspace after perturbing a tool library's module set, then verify affected builds complete without the runtime panic or backtrace.