## 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

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

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

#### 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)?

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

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: May 13 2021 at 23:16 UTC