RFC: Documentation page for collecting troubleshooting solutions

[Shreyas4991]

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.

[david-christiansen]

I think that this is generally a very good idea - things that are useful for all Lean users should really be in one centralized location.

Ideally, these issues won't happen at all for anyone, but we're clearly not there yet, and probably never will be 100%.

There's two things I'd like to think about:

1. How do we know that the problem is affecting people? If users are no longer affected by a given problem, then we're unlikely to hear that the problem doesn't happen anymore. We risk either not knowing that a problem affects lots of people (and thus underprioritizing a fix), or not knowing that it's not an issue anymore, and then accumulating a page full of irrelevant suggestions.
2. How do we check the quality and general risk profile of the workarounds proposed? For instance, if someone says that a particular piece of security software is causing the problem, and then we recommend disabling it, that might cause problems. We won't have access to every machine to test it.

It's probably fine if the answers to both questions are "we use our best judgment", but it would be great if we had an even better answer.

I'll follow up with the team.

[Shreyas4991]

1. This answer is non-trivial. But the problems can be reported by those who teach at university lectures and workshops for one example. Another method could be to check if this issue is being reported about on zulip more than a handful of times. For example lake issues are often brought up on zulip.
2. For this question "we use our best judgment" is probably the optimal answer in the medium term. Any solution for a problem will carry risks. "Install this version of curl" or "override your package manager's version of this CLI tool" are not ideal solutions, but fixes are needed to get lean running on users' systems in the shortrun. Providing a standard virtual machine might overcome some of these problems, but they also create another class of problems to solve.

[Shreyas4991]

I have a further proposal in response to both questions: With the exception of the issues that already in the leanprover community docs and lean docs, new issues will have to be introduced and discussed first on a topic in the relevant zulip stream. The response to each question on the webpage must link to the relevant zulip threads. This way users can make a more informed decision about using our solutions. This is a stopgap, and in the long run only security audits by domain experts can detect non-trivial problems. But having a discussion can bring up these issues to the forefront.