Suggested words for linkify

Stream: Zulip meta

[Eric Taucher]

leanproject
tutorial

[Mario Carneiro]

what do you want them to link to?

[Eric Taucher]

Mario Carneiro said:

what do you want them to link to?

Good question. As I am still learning Lean my self and there seems to be many possible choices, my guess would probably go down in history as He chose poorly.

Perhaps a vote by the community.

[Eric Taucher]

For tutorial I mostly like this one https://github.com/leanprover-community/tutorials as it is not tied to an IDE but if read by a new user would raise the question, where to enter leanproject get tutorials That is clearly answered in this YouTube video but a link to the middle of a video is even more confusing. Perhaps it needs a new page on the community web site https://leanprover-community.github.io/

[Eric Taucher]

For leanproject this one https://leanprover-community.github.io/leanproject.html is a clear leader as it is like a Unix man page but again for a new user does not explain how to install leanproject which is answered in this YouTube video. If the noted page included a section connecting the dots on what a leanproject is (think file structure with leanpkg.toml), in addition to the existing what the leanproject command does and adds a section on how to install leanproject then that would get my vote.

[Patrick Massot]

Don't forget there is also https://leanprover-community.github.io/install/project.html

[Patrick Massot]

The one you mentioned is indeed more like a man page.

[Eric Taucher]

Patrick Massot said:

Don't forget there is also https://leanprover-community.github.io/install/project.html

Thanks. :joy:
How can I forget when I don't even know.

[Patrick Massot]

You should have been brought there by https://leanprover-community.github.io/get_started.html#regular-install

[Eric Taucher]

For leanproject I agree with @Patrick Massot suggestion of https://leanprover-community.github.io/install/project.html. It has the links to the necessary information including the other page I like.

[Eric Taucher]

For tutorial, https://github.com/leanprover-community/tutorials seems to be the best fit. If one follows the instructions in links all should make sense. Since the option for changes is always on the table, it can adapt to feedback.

[Eric Taucher]

Mario Carneiro said:

what do you want them to link to?

leanproject - https://leanprover-community.github.io/install/project.html
tutorial - https://github.com/leanprover-community/tutorials

[Julian Berman]

There's also an existing glossary#leanproject

[Julian Berman]

Which maybe should itself be updated to include a link to that project page...

[Julian Berman]

https://github.com/leanprover-community/leanprover-community.github.io/pull/229