Troubleshooting mathlib

Stream: new members

[Stuart Presnell]

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]

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

[Julian Berman]

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]

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]

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]

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

[Stuart Presnell]

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