Zulip Chat Archive

Stream: general

Topic: Troubleshooting Page

Shreyas Srinivas (Oct 14 2023 at 17:27):

Hello Everyone,
I am collecting a list of common issues and fixes to attempt. One example is Antivirus software that manufacturers unnecessarily add to people's computers which block lake or lean. If you have more, please collect them here. If possible please Format your message as :

#### Issue
Please describe the problem you experienced here.

#### Solution
Please describe the solution that worked here in reasonable details

Shreyas Srinivas (Oct 14 2023 at 17:29):

The type of errors we describe here will be the ones that cause trouble with installation and cause VSCode to throw errors at us. But naturally we can broaden how we interpret this. I am collecting a few issues right now to add to the PR.

Patrick Massot (Oct 15 2023 at 18:01):

This is a nice idea, and would unclutter a bit our installation pages which already contain some troubleshooting instructions. However you should coordinate with @David Thrane Christiansen who is working on documentation and @Marc Huisinga who is working on the extension. The mathlib maintainer team really hopes that, in the not too distant future, all the installation-related pages of the community website will simply disappear. The current duplication of instructions is very confusing for new users, and create lots of extra work and frustration. If we are optimistic then we can think that in a couple of weeks all the installation pages of the community website will be replaced with a link to a lean-lang.org webpage saying: install the extension and follow the walkthrough.

Shreyas Srinivas (Oct 15 2023 at 18:04):

This idea came from the other thread about internet connection issues that you initiated

Patrick Massot (Oct 15 2023 at 18:05):

I understand, and it's great!

Patrick Massot (Oct 15 2023 at 18:06):

I'm only saying to be careful of coordination and don't waste energy in integrating this page on a sub-website that may disappear in one week. Collecting the content is perfectly fine and useful (assume Marc or David is not duplicating your efforts).

Shreyas Srinivas (Oct 15 2023 at 18:39):

@David Thrane Christiansen : what would your preferred approach be. Should I raise a PR for lean-lang website directly?

David Thrane Christiansen (Oct 16 2023 at 10:06):

Patrick Massot said:

The mathlib maintainer team really hopes that, in the not too distant future, all the installation-related pages of the community website will simply disappear. The current duplication of instructions is very confusing for new users, and create lots of extra work and frustration. If we are optimistic then we can think that in a couple of weeks all the installation pages of the community website will be replaced with a link to a lean-lang.org webpage saying: install the extension and follow the walkthrough.

I really hope this too! I'll follow up with the team on website procedures, I haven't updated it yet myself. But the docs clearly belong in one place, and they'll be useful outside the mathlib context, so it should be the main Lean site.

David Thrane Christiansen (Oct 16 2023 at 10:09):

Shreyas Srinivas said:

David Thrane Christiansen : what would your preferred approach be. Should I raise a PR for lean-lang website directly?

I think that's a good approach - thank you! Though I would expect that it would fit better here: https://lean-lang.org/lean4/doc/quickstart.html

David Thrane Christiansen (Oct 16 2023 at 10:09):

In any case, if you get me the content, I can make sure it goes in the right place. Thank you!

Shreyas Srinivas (Oct 16 2023 at 13:14):

@David Thrane Christiansen : Issue raised https://github.com/leanprover/lean4/issues/2698

Shreyas Srinivas (Oct 16 2023 at 13:14):

If agreed, I will follow up with a PR

David Thrane Christiansen (Oct 16 2023 at 13:15):

Thanks! I'll make sure it gets the right attention

Shreyas Srinivas (Oct 16 2023 at 13:17):

It might be a nice idea to create a separate stream called Toolchain/Installation issues that we can redirect users to if they don't find answers on the troubleshooting page @Patrick Massot

Patrick Massot (Oct 16 2023 at 13:47):

We usually use the new members stream for installation issues but we could indeed have a dedicated stream.

Shreyas Srinivas (Oct 16 2023 at 14:05):

that sounds like a good idea since toolchain issues also bother non-new members at the moment.

Eric Wieser (Oct 16 2023 at 14:58):

I think new members often can't tell apart installation issues from issues with their code, so if we made a new stream we'd just have installation issues across both streams

Shreyas Srinivas (Oct 19 2023 at 19:41):

A quick update:

1.I have collected some issues in the PR in the lean community site PR 370 379.

  1. Even if this content will eventually be on lean-lang.org, both sites currently use markdown so once the RFC goes through, making a fresh PR will not be too much work.
  2. Currently only @Floris van Doorn has offered comments on the PR and he says he doesn't see the reason for such a page.

Alex J. Best (Oct 19 2023 at 19:42):

https://github.com/leanprover-community/leanprover-community.github.io/pull/379 you mean?

Shreyas Srinivas (Oct 19 2023 at 19:43):

Yeah sorry 379

Shreyas Srinivas (Oct 19 2023 at 19:44):

Getting this PR through means we can put a link to it in vscode error messages, which I plan to PR once the page is up

Shreyas Srinivas (Oct 19 2023 at 20:13):

The idea to have such a page came up again today: https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Lean4.20cheatsheet/near/397240034

Shreyas Srinivas (Oct 19 2023 at 20:14):

This is where this discussion began first: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20extension.20update.20.22Commands.20.26.20Walkthrough.22/near/396528254

Last updated: Dec 20 2023 at 11:08 UTC