no leanpkg in lean4/stable?

Stream: lean4

[Omri Schwarz]

Hi, all. I'm moving to lean4 in time for AOC, and trying to run through some examples, and right now I"m with this gem:

def double (y : ℤ) :ℤ :=
y + y

Which complains of this:
16:4:
failed to synthesize instance
HAdd ℤ ℤ ?m.2742

Do we need to import preludes or something to get started?

[Adam Topaz]

I think the notation is introduced in Std or mathlib. What happens if you replace $\Z$ with Int?

[Adam Topaz]

Also #backticks

[Omri Schwarz]

Yup, that was the issue. Thanks!

[Damiano Testa]

You may want to add set_option autoImplicit false at the beginning of the file as well.

[Omri Schwarz]

Also, to actually stay true to the topic question:

```omri.schwarz@ARL-DYCPQTJJHN Advent % ls ~/.elan/toolchains/*/bin
/Users/omri.schwarz/.elan/toolchains/leanprover--lean4---nightly/bin:
clang lake ld64.lld lean leanc leanmake llvm-ar

/Users/omri.schwarz/.elan/toolchains/leanprover--lean4---stable/bin:
clang lake ld64.lld lean leanc leanmake llvm-ar

/Users/omri.schwarz/.elan/toolchains/stable/bin:
clang lake ld64.lld lean leanc leanmake llvm-ar
omri.schwarz@ARL-DYCPQTJJHN Advent %

Is leanpkg not part of the tooling for Lean 4?

[Kevin Buzzard]

The tooling for Lean 4 is elan and lake.

[Eric Wieser]

If you read documentation that led you to believe leanpkg would be there, can you link us to it so that we can correct it?

[Omri Schwarz]

This was in a mess of crashed browser tabs, so finding won't be easy, but I'm rechecking all the live docs and will flag anything I find

[Julian Berman]

Perhaps archiving a few more repositories in the leanprover-community org would be a good idea at this point. (In particular lean and doc-gen? Maybe others.) Specifically it'd make searches like https://github.com/search?q=org%3Aleanprover-community+leanpkg+NOT+is%3Aarchived&type=code a bit more useful.

[Eric Wieser]

I never even thought of using NOT is:archived in a search, so I'm not convinced we gain anything by optimizing for that case

[Eric Wieser]

Given that this is the third or fourth time that someone has complained that leanpkg is missing, and no one can ever tell us why they expected it in the first place, maybe the toolchain should just come with a leanpkg that prints an error message and a link to the lake docs

[Eric Wieser]

I created lean4#2872