RFC: Documentation page for collecting troubleshooting solutions

Proposal

I wish to add a page to the lean 4 manual that collects common problems and solutions with the lean installation. The goal is to maintain this page in a format similar to FAQs that can be used as a reference by community members and users to help out other users. Further, at the very top of the page, users will be informed that if they cannot find the solution to their problems here, they may raise the issue on Lean's zulipchat in the relevant stream.

Clear and detailed description of the proposal. Consider the following questions:

• User Experience: It provides users a distilled collection of Q&As that they can quickly reference to fix common issues. On the one hand users don't have to search through zulip and experienced users have a common resource to help each other for common problems. As a follow up, the idea is to add a troubleshooting link in vscode extension error messages that will take users straight to this page. Future proposals might included opening this page within the documentation viewer of the extension.

• Beneficiaries: Primarily new users who are just setting up lean and related projects and encounter issues that stem from their system setup, for example antiviruses, network management tools, package manager issues etc?

• Maintainability: This is a documentation page. The relevant decisions on maintenance are up to the documentation team. I can volunteer to update this page on a weekly basis if this is welcome. A zulip thread has been created for discussing issues that should be added here.

Community Feedback

There are two relevant zulip threads for this

• The relevant portion of the first thread began with a request that the new vscode extension features provide specific solutions to all possible externally caused problems and solutions. Subsequent discussion considered the difficulties of adding a check at each point a lake command is called, and the scalability nightmare of continuously identifying all the issues that even common anti-virus software might cause and linking to solutions from within vscode. I proposed that even if we could simply link to a troubleshooting page which collects common issues, we could substantially simplify user experience. FRO member @mhuisi accepted this suggestion. A first step towards implementing this solution is to have a troubleshooting page online
• The second thread discussed the location of this page. Although an initial PR was made on the lean community website, it was pointed out that this trouble shooting page should be on the lean webpage. @david-christiansen agreed that I could make a PR for this on the lean documentation webpage.

Impact

The feature provides users a quickly accessible collection of common issues that they may face when using lean and solutions for them. I expect the following results:

• Low latency and low anxiety problem resolution for common problems
• Fewer zulip threads that experienced users need to respond to for similar queries.

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the Lean manual and documentation webpage location, then read the linked Zulip discussions about page placement and scope. Define the troubleshooting FAQ's initial topics and maintenance process with the documentation team; done means a published page that provides common installation solutions and directs unresolved issues to Zulip.