Clearing Installation Process

Stream: lean4

[TAWSIF AHMED]

I had a request to the creators, I used lean couple of months back and came back now to learn it better and write maths stuff with it. What I encountered was a problem I had before in my first attempt.

lean in general is very hard to install. Not from a technical perspective rather from an user perspective. the installation process is all over the place and I am often confused what went wrong and what might be broken. VS Code installation module is amazing yet without the proper windows binaries, VS code installation does not work much.

I have currently elan, lean etc installed yet can't seem to use it for a single bit.

Complains: I don't mind having to install modules manually. I think most does not because anyone who wants to use lean have a relatively good technical background and obviously not starting out with programming.

Second, if common issues with elan and updates are presented in a singular website that will be extremely helpful. I know the community is fantastic yet asking questions everytime is not the best way of resolving something. (if something is too simple)

Third, could we get a single standalone lean guide. And a detail documentation like we receive with Python? Because I am extremely confused what to learn and what not because something seems to not work on my VS code setup yet works on the online lean editor. And there's so much tutorials and all were greatly different from each other. I am constantly struggling to keep up, rather than to learn and focus on my work, my productivity is low and I am trying to grasp what works anyways in the first place.

Pointers: I understand those who maintain the language "lean" they have other important activities. Yet, I will highlight, lean is powerful and a great tool to do proof of mathematical concepts yet the tool is of no-use, if the basics can't be learnt Or known.

Suggestions:

1. Can we receive a simple install and uninstallation process for lean
2. Standard errors be documented and listed in the official website
3. A proper documentation about the modules of the language
4. A good documentation about the libraries
5. VS Code installation method be deprecated?

I would be happy, if the authors take a look into the suggestions, looking forward what the community has to comment about this

[Kevin Buzzard]

Take a look at the community pages here and see if they're what you want.

[Mario Carneiro]

It would be helpful to describe more precisely what you read, what you tried, and what you saw as a result