fix: lake: await needs before processing module headers

[tydeu]

This PR changes Lake's module import graph processing to await the completion of any needs targets or other extra dependencies (such as cloud releases). This both enables the needs targets to influence header processing and prevents them from racing with said processing.

Known Limitation: This PR currently blocks on the needs targets rather than running the import processing in a callback. This is done to keep import processing simple and in a single thread. If this proves to be a performance issue, this can be restructured in a future PR with a more sophisticated refactor.

Closes #13598

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-02 07:40:23)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13601 build failed against this PR. (2026-05-02 08:27:03) View Log