How to install leanpkg

Stream: lean4

[Jo Liss]

Does leanpkg work with Lean 4? How do I install it?

(I made a StackOverflow question for this so the answer can be preserved on Google: https://stackoverflow.com/questions/76877068/how-to-install-leanpkg-with-elan-and-lean-4)

[Mauricio Collares]

leanpkg has been replaced by lake in Lean 4

[Pedro Sánchez Terraf]

Jo Liss said:

Does leanpkg work with Lean 4? How do I install it?

(I made a StackOverflow question for this so the answer can be preserved on Google: https://stackoverflow.com/questions/76877068/how-to-install-leanpkg-with-elan-and-lean-4)

Note that there is also PA.SE.

[Anatole Dedecker]

Note also that some of the streams in Zulip (those with a "world" icon next to their name) are archived and publicly accessible (and, I believe, referenced by Google)

[Pedro Sánchez Terraf]

I think Google search does not work here. Which is a pity, because the native search engine does not really work with me :sad:

[Julian Berman]

I think https://leanprover-community.github.io/archive/ is meant to be the replacement / fix for that (which is driven by https://github.com/leanprover-community/archive and which I think follows the recommendation from https://zulip.com/help/public-access-option#caveats which basically mentions that search engines can't index Zulip yet.)

[Pedro Sánchez Terraf]

Julian Berman said:

I think https://leanprover-community.github.io/archive/ is meant to be the replacement / fix for that (which is driven by https://github.com/leanprover-community/archive and which I think follows the recommendation from https://zulip.com/help/public-access-option#caveats which basically mentions that search engines can't index Zulip yet.)

I've just tried to perform the following Google search (for something I actually want to know): activate all linters site:https://leanprover-community.github.io/archive/ and it returns (for my search bubble) only 4 useless hits. Do you know an alternative way to search something like that?