live lean-lang broken

Stream: mathlib4

[Sébastien Gouëzel]

When opening the following box

import Mathlib

with live.lean-lang.org using the arrow on the top-right (View in Lean4 playground), it complains that it can't find Mathlib

[Rémy Degenne]

It fails on "Latest Mathlib" but works on "Mathlib stable"

[Etienne Marion]

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

[Edward van de Meent]

Wait, still?

[Kim Morrison]

(Fixed now.)