Zulip Chat Archive

Stream: general

Topic: leanpkg upgrade not working for me


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?

Patrick Massot (Oct 08 2019 at 15:45):

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

Patrick Massot (Oct 08 2019 at 15:45):

please post leanpkg.toml

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.

Kevin Buzzard (Oct 08 2019 at 15:45):

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

Kevin Buzzard (Oct 08 2019 at 15:46):

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

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

Patrick Massot (Oct 08 2019 at 15:47):

and don't forget to leanpkg configure after modifying this


Last updated: Dec 20 2023 at 11:08 UTC