Zulip Chat Archive

Stream: new members

Topic: Troubleshooting mathlib

Stuart Presnell (Dec 07 2021 at 16:51):

Is there a good guide to troubleshooting the common problems people run into when using mathlib/leanproject/github/VS Code? Things like the 'orange bar of doom' and the Failed to fetch mathlib oleans error message. Googling "Troubleshooting mathlib" brings up the "Using leanproject" page (https://leanprover-community.github.io/leanproject.html), but the advice there under "Troubleshooting" is just "ask on Zulip"!

Julian Berman (Dec 07 2021 at 16:53):

There's some short notes for the most common case in glossary#orange-bar-of-hell which come from @Rob Lewis

Julian Berman (Dec 07 2021 at 16:53):

I think the advice there in Troubleshooting is meant more for general obtuse Python errors more so than the typical problems which have to do with not having a local olean cache

Stuart Presnell (Dec 07 2021 at 17:03):

Since that seems to be the only relevant page that's returned by the Google search it might be useful to have a version of the glossary#orange-bar-of-hell text (or a link to it) in the Troubleshooting section. Or else have a more general dedicated Troubleshooting page addressing the various "Help! My mathlib got stuck!" problems that people run into.

Julian Berman (Dec 07 2021 at 18:05):

I think that's a decent idea yeah! I agree that the glossary is not the first place someone will look for that info. Perhaps a PR to the page you found is something you wouldn't mind sending?

Julian Berman (Dec 07 2021 at 18:05):

(Meanwhile -- did that fix the problem for you? Hope so?)

Stuart Presnell (Dec 07 2021 at 20:31):

I've just PR'ed a suggested addition to the page.

Last updated: Dec 20 2023 at 11:08 UTC