Zulip Chat Archive

Stream: general

Topic: leanpkg upgrade giving me 3.4.2 branch


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 09 2019 at 16:22):

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

view this post on Zulip 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$

view this post on Zulip 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

view this post on Zulip 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....

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 09 2019 at 16:53):

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

view this post on Zulip Patrick Massot (Feb 09 2019 at 17:33):

It should be ok

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 10 2019 at 01:11):

why are you trying to push the changes to the remote

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:12):

because leanpkg upgrade is downgrading me

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 10 2019 at 01:13):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:15):

Can't I track master?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:17):

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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:17):

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

view this post on Zulip 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)?

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:18):

I vote yes

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:18):

Why would anyone vote no?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:18):

ultimately I want leanpkg upgrade to take me to master

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:18):

Oh I see

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:19):

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

view this post on Zulip Mario Carneiro (Feb 10 2019 at 01:19):

I vote yes for auto update

view this post on Zulip Mario Carneiro (Feb 10 2019 at 01:19):

especially with the new olean releases

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 10 2019 at 01:20):

But make sure we only run this stuff on master branch

view this post on Zulip 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

view this post on Zulip Simon Hudon (Feb 10 2019 at 01:21):

That won't be hard

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:23):

(or even better, fixes things)

view this post on Zulip Simon Hudon (Feb 10 2019 at 01:43):

How do you get leanpkg to track lean-3.4.2?

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:43):

it does it by default as far as I can see

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:43):

lean_version = "3.4.2"

in leanpkg.toml

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:44):

if I understood correctly

view this post on Zulip Simon Hudon (Feb 10 2019 at 01:44):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:46):

This is in a project with mathlib as a dependency

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:46):

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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:47):

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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 01:47):

but that's what I want to do.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 15:58):

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


Last updated: May 13 2021 at 23:16 UTC