import Mathlib broken on web editor in v4.20.0rc-2

Stream: mathlib4

[Jovan Gerbscheid]

When I write import Mathlib in the "latest Mathlib" (the default) in the web editor I get this error:

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/Cli/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/batteries/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/Qq/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/aesop/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/importGraph/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/plausible/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/packages/mathlib/.lake/build/lib/lean
/home/lean4web/build/deploy-2025-05-05T12-00-16+00-00/mathlib-demo/.lake/build/lib/lean
/home/lean4web/.elan/toolchains/leanprover--lean4---v4.20.0-rc2/lib/lean
/lean/lib/lean

[Damiano Testa]

I noticed that lake build changed the way in which the paths are displayed: could the error be a consequence of this change?

[Yakov Pechersky]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60import.20Mathlib.60.20not.20working.20in.20.60live.2Elean-lang.2Eorg.60.3F