Zulip Chat Archive

Stream: new members

Topic: no nightly archive found


view this post on Zulip Luis O'Shea (Nov 17 2019 at 22:01):

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.

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 22:58):

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

view this post on Zulip Kevin Buzzard (Nov 17 2019 at 22:59):

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

view this post on Zulip Luis O'Shea (Nov 18 2019 at 04:27):

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).

view this post on Zulip Simon Hudon (Nov 18 2019 at 05:33):

What is the rest of your leanpkg.toml file?

view this post on Zulip Luis O'Shea (Nov 19 2019 at 00:55):

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"}

view this post on Zulip Bryan Gin-ge Chen (Nov 19 2019 at 01:01):

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.

view this post on Zulip Bryan Gin-ge Chen (Nov 19 2019 at 01:05):

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.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 07:25):

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

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 09:15):

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

view this post on Zulip Kevin Buzzard (Nov 20 2019 at 13:13):

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.

view this post on Zulip Luis O'Shea (Nov 21 2019 at 01:20):

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

view this post on Zulip Kevin Buzzard (Nov 21 2019 at 07:32):

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


Last updated: May 16 2021 at 20:13 UTC