Lean Web Editor and libraries outside mathlib

Stream: new members

[Matt Diamond]

Will the Lean web editor (https://live.lean-lang.org) ever have the ability to import projects outside of Mathlib? I ask because certain modules are being deprecated in favor of external libraries (e.g. Mathlib.SetTheory.Surreal.Basic is superseded by the CombinatorialGames repo), so if these modules are dropped entirely then the web editor will no longer have access to them.

Also, I just think it would be a cool feature to have.

[Kim Morrison]

Yes, this is coming. :-)