Lake build clean build with artifact cache leads to "missing data file"

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Steps to Reproduce

Start with:

lake +nightly-2026-07-17 new test lib
cd test
export LAKE_ARTIFACT_CACHE=true
lake cache clean # just to be sure

Add the following dependency to lakefile.toml:

[[require]]
name = "verso"
git = "https://github.com/leanprover/verso"
rev = "nightly-testing"

Then:

echo "import VersoManual.InlineLean" > Test.lean
lake build
lake clean
lake build

Finally open .lake/packages/verso/src/verso-manual/VersoManual/InlineLean.lean in VSCode. That leads to "missing data file for module MultiVerso.Manifest".

Versions

Output of #version or #eval Lean.versionString:

Lean 4.34.0, commit 79bec6d064d8672cb10864cad3d9fd054b6917ae
Target: x86_64-unknown-linux-gnu`

OS version, if not using live.lean-lang.org: Arch Linux.

Additional Information

Happens at least with v4.33.0-rc1, too.

Start by reproducing the commands in the issue with Lean 4.34.0 and LAKE_ARTIFACT_CACHE=true, then compare the first build, lake clean, and second build. Inspect the generated artifact data for VersoManual.InlineLean.lean and the reported MultiVerso.Manifest module. Done means a clean rebuild completes and VSCode opens the file without a missing data file error.