no nightly archive found

Stream: new members

[Luis O'Shea]

Downloading a local copy of KB's M1F Example Sheets repo I ran into a small problem when running update-mathlib which errored out saying "Error: no nightly archive found". I believe this is benign; at any rate I was able to run leanpkg build successfully, and the lean files seemed to open in VS Code without errors. Assuming this is as expected, I'm mostly reporting this for other beginners (like me).

Below is what I did and its output:

$ git clone https://github.com/ImperialCollegeLondon/M1F_example_sheets.git
Cloning into 'M1F_example_sheets'...
remote: Enumerating objects: 12, done.
remote: Counting objects: 100% (12/12), done.
remote: Compressing objects: 100% (12/12), done.
remote: Total 942 (delta 4), reused 0 (delta 0), pack-reused 930
Receiving objects: 100% (942/942), 1.30 MiB | 7.42 MiB/s, done.
Resolving deltas: 100% (514/514), done.

$ cd M1F_example_sheets/

$ leanpkg configure
info: downloading component 'lean'
info: installing component 'lean'
configuring M1F_2018-19 0.1
mathlib: cloning https://github.com/leanprover/mathlib to _target/deps/mathlib
> mkdir -p _target/deps/mathlib
> git clone https://github.com/leanprover/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 13, done.
remote: Counting objects: 100% (13/13), done.
remote: Compressing objects: 100% (13/13), done.
remote: Total 27510 (delta 3), reused 1 (delta 0), pack-reused 27497
Receiving objects: 100% (27510/27510), 13.64 MiB | 11.51 MiB/s, done.
Resolving deltas: 100% (20453/20453), done.
> git checkout --detach 2a86b06b1853493ab4fb381514e7d1a3f4dfc54b    # in directory _target/deps/mathlib
HEAD is now at 2a86b06b fix(order/filter): tendsto_at_top only requires preorder not partial_order

$ update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Error: no nightly archive found

$ leanpkg build
configuring M1F_2018-19 0.1
mathlib: trying to update _target/deps/mathlib to revision 2a86b06b1853493ab4fb381514e7d1a3f4dfc54b
> git checkout --detach 2a86b06b1853493ab4fb381514e7d1a3f4dfc54b    # in directory _target/deps/mathlib
HEAD is now at 2a86b06b fix(order/filter): tendsto_at_top only requires preorder not partial_order
> lean --make src
# Lots of warnings from files in src/ about declarations that use sorry.  No errors.

[Kevin Buzzard]

I can quite believe that that repo is older than the update-mathlib set-up.

[Kevin Buzzard]

Just do leanpkg upgrade or update or whatever it is that gets new mathlib. Then it might work

[Luis O'Shea]

I did a leanpkg upgrade (with no problems) and among other things it generated the following diff to leanpkg.toml:

-mathlib = {git = "https://github.com/leanprover/mathlib", rev = "2a86b06b1853493ab4fb381514e7d1a3f4dfc54b"}
+mathlib = {git = "https://github.com/leanprover/mathlib", rev = "7c5f282dcfe1e0f20050f4aae3b6bdf77a652a13"}

However update-mathlib continued to complain about "Error: no nightly archive found". Also leanpkg build errored out. So I think the right recipe for this repo is to do as I did the first time (which at the end of the day seems to work).

[Simon Hudon]

What is the rest of your leanpkg.toml file?

[Luis O'Shea]

My leanpkg.toml is

[package]
name = "M1F_2018-19"
version = "0.1"
lean_version = "nightly-2018-06-21"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", rev = "7c5f282dcfe1e0f20050f4aae3b6bdf77a652a13"}

[Bryan Gin-ge Chen]

This is probably the offending line:

lean_version = "nightly-2018-06-21"

This is a really old version of Lean. Currently update-mathlib can only supply Lean binaries for Lean 3.4.2.

[Bryan Gin-ge Chen]

Furthermore, the reason that leanpkg build errored out after leanpkg upgrade is that recent versions of mathlib are not compatible with versions of Lean before 3.4.2. So, if you change that line to this:

lean_version = "3.4.2"

Then both leanpkg build and update-mathlib should both work again.

[Kevin Buzzard]

So it's just the fact that it's a very old repo. I'll try and remember to update the toml on github

[Kevin Buzzard]

That repo is really old. Loads of the imports don't work any more.

[Kevin Buzzard]

OK so I am hoping that if you pull the updated repo, this is fixed. Thanks for pointing this out. Some of the proofs had broken but I just fixed them all.

[Luis O'Shea]

Yes, thank you! I think this is now fixed. See below for output, in case anyone is curious. (All the output from leanpkg build is warnings, mostly about sorry and a few uses of #exit which can all be traced to KB's commit mathlib broke my 2017 soln; in other words, it all seems good.)

$ git clone https://github.com/ImperialCollegeLondon/M1F_example_sheets.git M1F_example_sheets3
Cloning into 'M1F_example_sheets3'...
remote: Enumerating objects: 56, done.
remote: Counting objects: 100% (56/56), done.
remote: Compressing objects: 100% (51/51), done.
remote: Total 986 (delta 11), reused 24 (delta 4), pack-reused 930
Receiving objects: 100% (986/986), 1.32 MiB | 6.99 MiB/s, done.
Resolving deltas: 100% (521/521), done.

$ cd M1F_example_sheets3/

$ leanpkg configure
configuring M1F_2018-19 0.1
mathlib: cloning https://github.com/leanprover/mathlib to _target/deps/mathlib
> mkdir -p _target/deps/mathlib
> git clone https://github.com/leanprover/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 45, done.
remote: Counting objects: 100% (45/45), done.
remote: Compressing objects: 100% (35/35), done.
remote: Total 27548 (delta 18), reused 18 (delta 10), pack-reused 27503
Receiving objects: 100% (27548/27548), 13.69 MiB | 10.56 MiB/s, done.
Resolving deltas: 100% (20473/20473), done.
> git checkout --detach d67e527adc99837b731799190fdc7cbeb596254f    # in directory _target/deps/mathlib
HEAD is now at d67e527a feat(algebra/group_power): prove Bernoulli's inequality for `a ≥ -2` (#1709)

$ update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Downloading nightly...
Extracting nightly...

$ leanpkg build
configuring M1F_2018-19 0.1
mathlib: trying to update _target/deps/mathlib to revision d67e527adc99837b731799190fdc7cbeb596254f
> git checkout --detach d67e527adc99837b731799190fdc7cbeb596254f    # in directory _target/deps/mathlib
HEAD is now at d67e527a feat(algebra/group_power): prove Bernoulli's inequality for `a ≥ -2` (#1709)
> lean --make src
# several dozen warnings

[Kevin Buzzard]

The warnings are just because a lot of the questions have sorry. I believe there are no errors