Zulip Chat Archive

Stream: general

Topic: leanpkg upgrade giving me 3.4.2 branch


Kevin Buzzard (Feb 09 2019 at 16:22):

I use elan. In a project I have, which I want to keep up to date with mathlib head, leanpkg upgrade gives me the lean-3.4.2 branch of mathlib. Why is this happening? My leanpkg.toml contains the line lean_version = "3.4.2". Is that the problem? If so, what should it say?

Kevin Buzzard (Feb 09 2019 at 16:22):

the mathlib lean-3.4.2 branch is currently 9 days behind HEAD.

Kevin Buzzard (Feb 09 2019 at 16:23):

Changing 3.4.2 to master in my leanpkg.toml gives me

$ leanpkg upgrade
error: override toolchain 'master' is not installed
info: caused by: the toolchain file at '/home/buzzard/Encfs/Computer_languages/Lean/lean-projects/M1P1-lean/leanpkg.toml' specifies an uninstalled toolchain
buzzard@bob:~/Lean/lean-projects/M1P1-lean$

Kevin Buzzard (Feb 09 2019 at 16:26):

With 3.4.2 I get

$ leanpkg upgrade
mathlib: trying to update _target/deps/mathlib to revision 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609
> git checkout --detach 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609    # in directory _target/deps/mathlib
HEAD is now at 50a03f7 chore(test): fix test directory structure
configuring M1P1-lean 0.1
mathlib: trying to update _target/deps/mathlib to revision 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609
> git checkout --detach 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609    # in directory _target/deps/mathlib
HEAD is now at 50a03f7 chore(test): fix test directory structure
buzzard@bob:~/Lean/lean-projects/M1P1-lean$

which is precisely https://github.com/leanprover-community/mathlib/tree/lean-3.4.2

Kevin Buzzard (Feb 09 2019 at 16:27):

buzzard@bob:~/.elan/toolchains$ ls
3.3.0  3.4.2  nightly-2018-06-21  stable

Hmm....

Kevin Buzzard (Feb 09 2019 at 16:28):

lean_version = "stable"

...

$ leanpkg upgrade

WARNING: Lean version mismatch: installed version is 3.4.2, but package requires stable

mathlib: trying to update _target/deps/mathlib to revision 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609
> git checkout --detach 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609    # in directory _target/deps/mathlib
HEAD is now at 50a03f7 chore(test): fix test directory structure
From https://github.com/leanprover-community/mathlib
 * [new tag]         bin-20190209-162751-484d864 -> bin-20190209-162751-484d864

WARNING: Lean version mismatch: installed version is 3.4.2, but package requires stable

configuring M1P1-lean 0.1
mathlib: trying to update _target/deps/mathlib to revision 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609
> git checkout --detach 50a03f76bb89ee5cf9d9703f78e1eb2139d9b609    # in directory _target/deps/mathlib
HEAD is now at 50a03f7 chore(test): fix test directory structure

GAARGH

Kevin Buzzard (Feb 09 2019 at 16:33):

I think I can push to lean-3.4.2 but I am scared I'll screw up.

Kevin Buzzard (Feb 09 2019 at 16:53):

If I do (within my clone of leanprover-community/mathlib)

$ git checkout master
$ git pull
$ git checkout lean-3.4.2
$ git pull
$ git merge master
$ git push

will that be a good thing or will something bad happen?

Kevin Buzzard (Feb 09 2019 at 16:53):

There's a chance it will solve my problem, at least temporarily

Patrick Massot (Feb 09 2019 at 17:33):

It should be ok

Kevin Buzzard (Feb 10 2019 at 01:08):

 ! [remote rejected] lean-3.4.2 -> lean-3.4.2 (protected branch hook declined)
error: failed to push some refs to 'git@github.com:leanprover-community/mathlib.git'

Rotten luck. OK so I'm out of ideas.

Mario Carneiro (Feb 10 2019 at 01:11):

why are you trying to push the changes to the remote

Kevin Buzzard (Feb 10 2019 at 01:12):

because leanpkg upgrade is downgrading me

Kevin Buzzard (Feb 10 2019 at 01:12):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanpkg.20upgrade.20giving.20me.203.2E4.2E2.20branch/near/157935869

Mario Carneiro (Feb 10 2019 at 01:13):

that's even if you move up your local branch?

Kevin Buzzard (Feb 10 2019 at 01:14):

I don't have a local branch in my repo with mathlib as a dependency. I just have a mathlib with a detached head.

Kevin Buzzard (Feb 10 2019 at 01:15):

I don't want to be copying commit hashes into my leanpkg.toml manually, I just want leanpkg upgrade to do everything for me. I am in my own project with mathlib as a dependency and leanpkg upgrade drags me back to the lagging-behind 3.4.2. I just want to track HEAD

Kevin Buzzard (Feb 10 2019 at 01:15):

Can't I track master?

Mario Carneiro (Feb 10 2019 at 01:16):

I recall Sebastian giving some reasons for why it shouldn't be done, and me being skeptical

Kevin Buzzard (Feb 10 2019 at 01:16):

$ more leanpkg.toml
[package]
name = "M1P1-lean"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "50a03f7
6bb89ee5cf9d9703f78e1eb2139d9b609"}
buzzard@bob:~/Lean/lean-projects/M1P1-lean$

Whenever I type leanpkg upgrade my toml is pulled back to this

Kevin Buzzard (Feb 10 2019 at 01:16):

But now we have control of the repo in a better way, can we just write a hook to make 3.4.2 track master?

Kevin Buzzard (Feb 10 2019 at 01:17):

This was what we couldn't do before, right?

Kevin Buzzard (Feb 10 2019 at 01:17):

Does the change to leanprover-community make all this easier to handle?

Simon Hudon (Feb 10 2019 at 01:18):

Do we want lean-3.4.2 to point to the latest nightly (which I'm setting up now)?

Kevin Buzzard (Feb 10 2019 at 01:18):

I vote yes

Kevin Buzzard (Feb 10 2019 at 01:18):

Why would anyone vote no?

Simon Hudon (Feb 10 2019 at 01:18):

The benefit is that tracking lean-3.4.2 should always give you access to binary releases

Kevin Buzzard (Feb 10 2019 at 01:18):

ultimately I want leanpkg upgrade to take me to master

Kevin Buzzard (Feb 10 2019 at 01:18):

Oh I see

Simon Hudon (Feb 10 2019 at 01:19):

I have no idea why not to do it but the other developers have more imagination than me

Kevin Buzzard (Feb 10 2019 at 01:19):

I think I'd rather have today's commit and then spend 10 minutes compiling

Mario Carneiro (Feb 10 2019 at 01:19):

I vote yes for auto update

Mario Carneiro (Feb 10 2019 at 01:19):

especially with the new olean releases

Kevin Buzzard (Feb 10 2019 at 01:19):

actually I think Id rather have yesterday's commit and not compile

Kevin Buzzard (Feb 10 2019 at 01:20):

but I don't think I want to be 66 commits behind -- some of those commits are mine and I want them in my repo

Mario Carneiro (Feb 10 2019 at 01:20):

But make sure we only run this stuff on master branch

Mario Carneiro (Feb 10 2019 at 01:20):

PRs and other things also trigger travis but shouldn't release oleans or move lean-3.4.2

Simon Hudon (Feb 10 2019 at 01:21):

That won't be hard

Kevin Buzzard (Feb 10 2019 at 01:22):

What we're talking about here is basically the perfect solution for me. I want to keep moving my repos along with master as they are developed, so I quickly see when an update breaks things.

Kevin Buzzard (Feb 10 2019 at 01:23):

(or even better, fixes things)

Simon Hudon (Feb 10 2019 at 01:43):

How do you get leanpkg to track lean-3.4.2?

Kevin Buzzard (Feb 10 2019 at 01:43):

it does it by default as far as I can see

Kevin Buzzard (Feb 10 2019 at 01:43):

lean_version = "3.4.2"

in leanpkg.toml

Kevin Buzzard (Feb 10 2019 at 01:44):

if I understood correctly

Simon Hudon (Feb 10 2019 at 01:44):

Cool! Do you have to call leanpkg upgrade or does it upgrade its packages automatically?

Kevin Buzzard (Feb 10 2019 at 01:46):

When I type leanpkg upgrade (which I do occasionally, if I am interested in a recent commit, or if I feel like I want to check my project still compiles against mathlib head), it pulls mathlib and switches to the commit corresponding to the lean_version, as far as I can see

Kevin Buzzard (Feb 10 2019 at 01:46):

This is in a project with mathlib as a dependency

Kevin Buzzard (Feb 10 2019 at 01:46):

i.e. where I am 99% of the time

Kevin Buzzard (Feb 10 2019 at 01:47):

If I understand correctly, it is not recommended that there be a way to track master

Kevin Buzzard (Feb 10 2019 at 01:47):

but that's what I want to do.

Simon Hudon (Feb 10 2019 at 01:49):

With this new nightly system, we could in principle coordinate dependent packages so that they affix the lean-3.4.2 only when it works with the lean-3.4.2 version of mathlib.

Kevin Buzzard (Feb 10 2019 at 10:07):

I am not clear what the solution to my problem is yet. The docs for leanpkg say that leanpkg upgrade will update all dependencies to the latest upstream version. Currently they don't because of the existence of the lean-3.4.2 tag whose behaviour seems to be undefined. What do I do as an end user if I simply want to do the very natural thing of updating my dependencies because they just got a commit I want for my project?

Kevin Buzzard (Feb 10 2019 at 10:48):

Obviously I can just go into _target and fix things up myself, but then my leanpkg.toml becomes an unreliable witness to the situation, and this won't work for my clients anyway.

Reid Barton (Feb 10 2019 at 14:40):

What I do in practice is just edit the commit IDs in leanpkg.toml manually. Sometimes you want to do this anyways, because for example the latest commit of mathlib doesn't build, or when updating to the latest mathlib would cause a lot of breakage and you'd rather take smaller steps.

Kevin Buzzard (Feb 10 2019 at 15:51):

I know I can do this but then when I change the toml how do people like Patrick and Johan update their clones? They have to do the same sort of thing too, right? And what about the undergraduates who don't know what git is but clone my undergraduate analysis repo?

Patrick Massot (Feb 10 2019 at 15:53):

leanpkg.toml is included in the repository, so users who use git pull to get the latest version get this file. And then leanpkg build updates mathlib if needed

Kevin Buzzard (Feb 10 2019 at 15:58):

Oh! So I just avoid using upgrade and my problems go away??


Last updated: Dec 20 2023 at 11:08 UTC