leanpkg upgrade not working for me

Stream: general

[Kevin Buzzard]

I am with a student and when we type leanpkg upgrade on their project things seem to work fine. But when I then type update-mathlib in their repo I get Error: no nightly archive found. In _target/deps/mathlib I see all the latest commits. I thought that update-mathlib always worked now -- do I have to wait for something to compile or something?

[Patrick Massot]

It looks like it tries to use mathlib master instead of lean-3.4.2

[Patrick Massot]

please post leanpkg.toml

[Floris van Doorn]

I don't know if this an issue for update-mathlib but you can try checking out origin/lean-3.4.2.

[Kevin Buzzard]

Aah thanks Patrick. This is a super-old project.

[Kevin Buzzard]

lean_version = "nightly-2018-06-21" ;-)

[Patrick Massot]

Make sure this file ends with

lean_version = "3.4.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "c6fab42c36f65ff95a9043aa7aa6fb9bc4b4708c"}

[Patrick Massot]

and don't forget to leanpkg configure after modifying this