search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
54 stars 123 forks source link

Feat : Troubleshooting Page #379

Open Shreyas4991 opened 1 year ago

Shreyas4991 commented 1 year ago

In this PR I add a page to the website which accumulates common problems that users encounter with their lean installation. I further wish to link users from vscode error messages to this URL in a separate PR on the extension repository. Please see Zulip for the discussion that led to this PR.

fpvandoorn commented 1 year ago

I think this page could be a good idea (though some of the troubleshooting should be inlined in the relevant places).

However, I don't think we should merge this until there are a few helpful tips on the new page. Therefore, I'm marking this PR as awaiting-author for now.

Shreyas4991 commented 1 year ago

@fpvandoorn : there has been an update. You can find the summary in the RFC issue I raised. Basically it was suggested that this website is not the right place for toolchain issues. I would like to keep this PR around until a decision is made there on that issue.

Shreyas4991 commented 1 year ago

@fpvandoorn : For good measure I collected some common problems and added them. I can't seem to change labels, so I can't remove the awaiting-author label.

fpvandoorn commented 1 year ago

I think that these troubleshooting remarks are more useful when they are inlined with the rest of the instructions (maybe in a text box that is collapsed by default, but expandable).

Shreyas4991 commented 1 year ago

I think that these troubleshooting remarks are more useful when they are inlined with the rest of the instructions (maybe in a text box that is collapsed by default, but expandable).

Indeed they are useful there. But, in addition to the points made in the lean4 PR, we would like to collect these issues in one place so that we can give a link to it in VSCode error messages, especially in light of all the new features. Providing highly specific diagnoses for each error would be much more difficult. Additionally, there are other threads where people have suggested that such a page should exist.