Binary package not provided

Stream: new members

[Tianchen Zhao]

Ja_1941@MSI MINGW64 ~/desktop
$ git clone https://github.com/ChrisHughes24/Sylow.git
Cloning into 'Sylow'...
remote: Enumerating objects: 14, done.
Receiving objects:  64% (9/14)used 0 (delta 0), pack-reused 14 eceiving objects:  57% (8/14)
Receiving objects: 100% (14/14), 20.54 KiB | 244.00 KiB/s, done.
Resolving deltas: 100% (2/2), done.

Ja_1941@MSI MINGW64 ~/desktop
$ cd Sylow/

Ja_1941@MSI MINGW64 ~/desktop/Sylow (master)
$ lean configure
info: downloading component 'lean'
error: binary package was not provided for 'windows'

I have been working on one repository for some time and not cloning anything new. But today when I tried to clone something new, bash said "binary package was not provided for 'windows'". I looked at other posts about binary package not provided and people say it's a matter of time. Is it the same case for me here?

[Bryan Gin-ge Chen]

Hmm, the version of Lean specified in that package's leanpkg.toml is "nightly-2018-04-20". It looks like a binary is available here, however for some reason elan doesn't seem to be able to pick it up. You might try changing the version string to 3.4.1 and seeing if that works.

cc: @Sebastian Ullrich

[Tianchen Zhao]

Bryan Gin-ge Chen said:

Hmm, the version of Lean specified in that package's leanpkg.toml is "nightly-2018-04-20". It looks like a binary is available here, however for some reason elan doesn't seem to be able to pick it up. You might try changing the version string to 3.4.1 and seeing if that works.

cc: Sebastian Ullrich

How can I change the version string to 3.4.1? Does that mean I need to change the lean version in leanpkg.toml to "leanprover-community/lean:3.4.1"? It gives me the same error though. Does it have anything to do with my elan installaion? btw I don't understand specifically what's nightly and leanpkg toml. Where can I learn about them? Thank you.

[Kevin Buzzard]

This is a really old project. Does lean --make sylow.lean (and then wait for an hour) work?

[Kevin Buzzard]

This project is pre Leanproject so compilation will be harder.

[Bryan Gin-ge Chen]

Tianchen Zhao said:

How can I change the version string to 3.4.1? Does that mean I need to change the lean version in leanpkg.toml to "leanprover-community/lean:3.4.1"? It gives me the same error though. Does it have anything to do with my elan installaion? btw I don't understand specifically what's nightly and leanpkg toml. Where can I learn about them? Thank you.

Lean 3.4.1 predates leanprover-community/lean, so I was suggesting just changing the Lean version to 3.4.1 directly.

[Bryan Gin-ge Chen]

I can confirm that changing the line with `lean_version to:

lean_version = "3.4.1"

and then running leanproject build and waiting for a while (since we don't have olean files that go that far back) successfully builds the project. I'll open a PR. cc: @Chris Hughes

[Tianchen Zhao]

Kevin Buzzard said:

This is a really old project. Does lean --make sylow.lean (and then wait for an hour) work?

It still says binary package not provided, but changing the version to 3.4.1 make it work.

[Tianchen Zhao]

It works using 3.4.1 :tada: