Zulip Chat Archive

Stream: general

Topic: leanpkg upgrade not working for me


view this post on Zulip Kevin Buzzard (Oct 08 2019 at 15:44):

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?

view this post on Zulip Patrick Massot (Oct 08 2019 at 15:45):

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

view this post on Zulip Patrick Massot (Oct 08 2019 at 15:45):

please post leanpkg.toml

view this post on Zulip Floris van Doorn (Oct 08 2019 at 15:45):

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

view this post on Zulip Kevin Buzzard (Oct 08 2019 at 15:45):

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

view this post on Zulip Kevin Buzzard (Oct 08 2019 at 15:46):

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

view this post on Zulip Patrick Massot (Oct 08 2019 at 15:46):

Make sure this file ends with

lean_version = "3.4.2"
path = "src"

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

view this post on Zulip Patrick Massot (Oct 08 2019 at 15:47):

and don't forget to leanpkg configure after modifying this


Last updated: May 13 2021 at 20:13 UTC