Feat : Troubleshooting Page #379
Conversation
|
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 |
|
@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. |
|
@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 |
Fixed a mistake in command not found. the third instruction also works for Linux.
|
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. |
| * If you are on linux, currently the default shell in popular distributions like Ubuntu or Linux Mint is `bash`. In this case, run `source ~/.bashrc`. | ||
| * If this still doesn't work, logging out and logging in again should fix it. | ||
|
|
||
| ### InitializeSecurityContext error on Windows |
There was a problem hiding this comment.
Having this information in two different places feels like a recipe for confusion to me.
There was a problem hiding this comment.
Perhaps we could link to this paragraph from other pages. In such pages we have a section titled "Errors you might encounter" with links
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.