Zulip Chat Archive
Stream: mathlib4
Topic: polyrith does not work in the web editor
Eric Wieser (Nov 19 2023 at 18:50):
If you use polyrith, you get "Could not find Mathlib directory. Make sure the LEAN_SRC_PATH environment variable is set correctly."
Last updated: Dec 20 2023 at 11:08 UTC