leanpkg upgrade giving me 3.4.2 branch

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

Hmm....

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

It should be ok

[Kevin Buzzard]

 ! [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]

why are you trying to push the changes to the remote

[Kevin Buzzard]

because leanpkg upgrade is downgrading me

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

Can't I track master?

[Mario Carneiro]

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

[Kevin Buzzard]

$ 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]

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]

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

[Kevin Buzzard]

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

[Simon Hudon]

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

[Kevin Buzzard]

I vote yes

[Kevin Buzzard]

Why would anyone vote no?

[Simon Hudon]

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

[Kevin Buzzard]

ultimately I want leanpkg upgrade to take me to master

[Kevin Buzzard]

Oh I see

[Simon Hudon]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I vote yes for auto update

[Mario Carneiro]

especially with the new olean releases

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

But make sure we only run this stuff on master branch

[Mario Carneiro]

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

[Simon Hudon]

That won't be hard

[Kevin Buzzard]

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]

(or even better, fixes things)

[Simon Hudon]

How do you get leanpkg to track lean-3.4.2?

[Kevin Buzzard]

it does it by default as far as I can see

[Kevin Buzzard]

lean_version = "3.4.2"

in leanpkg.toml

[Kevin Buzzard]

if I understood correctly

[Simon Hudon]

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

[Kevin Buzzard]

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]

This is in a project with mathlib as a dependency

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but that's what I want to do.

[Simon Hudon]

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]

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]

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]

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]

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]

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]

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