updating mathlib without compiling is hard

Stream: general

[Kevin Buzzard]

I have a project with a dependency on mathlib. I want Patrick's lovely has_mem (set ℝ) (filter ℝ), which is in a recent mathlib. So I go to my project, type leanpkg upgrade and I find that mathlib is now back at Feb 23rd.

So I go into _target/deps/mathlib, checkout master, pull, look at the latest commit, edit my leanpkg.toml to point to this commit, then type update-mathlib and it says "no nightly archive found".

Now I don't know what to do. I know that it will be much better when someone who can build the infrastructure builds the infrastructure but I just want to get something working quickly now, and I'm sure this should be possible with a bit of hacking around.

How do I painlessly figure out the most recent commit that will make update-mathlib work? And once I've figured it out, which of (a) manually editing my toml so that it points to this mathlib commit and (b) manually switching to the correct commit in _target/deps/mathlib do I need to do, in order to get update-mathlib to work?

I just want the most recent commit for which I don't have to compile mathlib.

[Kevin Buzzard]

Oh! update-mathlib now works! So was I just unlucky somehow? I coincidentally pulled very quickly after a commit or something?

[Chris Hughes]

There was a commit very recently, so that may be the case.

[Patrick Massot]

Indeed the latest nighly is 14 minutes old The answer to the question was: go to https://github.com/leanprover-community/mathlib-nightly/releases, get the commit hash, modify the leanpkg.toml of your project, and run upodate-mathlib

[Patrick Massot]

Hopefully this answer will soon become unneeded

[Simon Hudon]

leanpkg upgrade followed by update-mathlib should also work.

[Patrick Massot]

No it won't work in general

[Patrick Massot]

unless you are very lucky

[Patrick Massot]

This is why we need a binary release for every commit

[Simon Hudon]

Why doesn't it work?

[Johan Commelin]

Because leanpkg upgrade moves to the latest commit of mathlib. And that one typically doesn't have an olean-release attached to it.

[Johan Commelin]

Ideally, leanpkg upgrade would update to latest mathlib, and call update-mathlib.

[Johan Commelin]

Alternatively, update-mathlib could edit the .toml to point to the latest olean-release of mathlib, and do the rest of its magic.

[Simon Hudon]

It should go to the latest commit on the lean-3.4.2 branch which get pushed when we make releases. They should all have a proper olean archive attached

[Johan Commelin]

Hmm... that didn't work when I last tried it.

[Johan Commelin]

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

[Johan Commelin]

@Simon Hudon :up:

[Simon Hudon]

That's odd. I'll have a look

[Simon Hudon]

I think there was probably a non-monotonic rebase about 11 days ago and now Travis fails every time it tries to push to lean-3.4.2. I pushed it manually.

[Simon Hudon]

It should now work if you do leanpkg upgrade and then update-mathlib

[Patrick Massot]

I can confirm it works in the perfectoid project (bringing it only 2 commits behind mathlib master)

[Simon Hudon]

:fireworks:

[Keeley Hoek]

Also if you want to track master you can do branch = 'master' in leanpkg.toml

[Kevin Buzzard]

I don't have any branch = anything in the toml of the perfectoid project.

[Kevin Buzzard]

I am not sure I want to track mathlib master, I want to track "the last release with some olean files" :-)

[Patrick Massot]

That's what we already do

[Kevin Buzzard]

hopefully

[Patrick Massot]

we don't need to change anything here (except we need people to stop pushing outdated tags)

[Kevin Buzzard]

Probably the next time I push anything I will push an outdated tag

[Kevin Buzzard]

I have a gazillion copies of community mathlib across various machines

[Patrick Massot]

running git tag -d 3.4.2 in each of them would help

[Kevin Buzzard]

I typed git branch -d lean-3.4.2 and Johan said it wasn't enough

[Kevin Buzzard]

but then the branch did not show up with git branch

[Patrick Massot]

You need new glasses

[Kevin Buzzard]

I typed git tag -d 3.4.2 and it looked like something succeeded

[Kevin Buzzard]

however Simon said there were a tonne of other tags which needed deleting

[Patrick Massot]

This is the correct one

[Kevin Buzzard]

and I can't see any of them in my branches

[Kevin Buzzard]

Oh so I don't need to worry about the other tags he mentioned?

[Patrick Massot]

what does git tag says?

[Kevin Buzzard]

$ git tag
bin-20190207-231626-1b7baba
bin-20190208-212100-4227f5c
bin-20190208-220606-64065f4
bin-20190208-221206-814cb03
bin-20190208-222309-650237b
bin-20190208-235057-8b51017
bin-20190209-020632-22c7179
bin-20190209-162751-484d864
bin-20190209-163013-088f753
bin-20190210-113848-ed4c536
bin-20190210-131553-d6f84da
bin-20190210-152455-c25122b
bin-20190210-171431-9b28db0
untagged-9164526c5fa59e86918d

[Kevin Buzzard]

$ git tag
bin-20190208-212100-4227f5c
bin-20190208-220606-64065f4
bin-20190208-221206-814cb03
bin-20190208-222309-650237b
bin-20190208-235057-8b51017
bin-20190209-020632-22c7179
bin-20190209-162751-484d864
bin-20190209-163013-088f753
bin-20190210-113848-ed4c536
bin-20190210-131553-d6f84da
lean-3.4.2
untagged-9164526c5fa59e86918d

in another one

[Kevin Buzzard]

I can go and find my laptop and give you a couple more

[Kevin Buzzard]

and then there's my work machine

[Kevin Buzzard]

they're everywhere

[Patrick Massot]

I think you can safely git tag | xargs git tag -d

[Patrick Massot]

You don't need any of these tags, they can only hurt

[Kevin Buzzard]

can there ever be a space in a tag?

[Patrick Massot]

no

[Kevin Buzzard]

Well this is a good step forward: I am tag-free on my home desktop

[Kevin Buzzard]

hey wait a second:

buzzard@bob:~/Lean/lean-projects/mathlib-community-master$ git tag
bin-20190208-212100-4227f5c
bin-20190208-220606-64065f4
bin-20190208-221206-814cb03
bin-20190208-222309-650237b
bin-20190208-235057-8b51017
bin-20190209-020632-22c7179
bin-20190209-162751-484d864
bin-20190209-163013-088f753
bin-20190210-113848-ed4c536
bin-20190210-131553-d6f84da
bin-20190210-152455-c25122b
bin-20190210-171431-9b28db0
untagged-9164526c5fa59e86918d
buzzard@bob:~/Lean/lean-projects/mathlib-community-master$ git tag | xargs git tag -d
Deleted tag 'bin-20190208-212100-4227f5c' (was 4227f5c)
Deleted tag 'bin-20190208-220606-64065f4' (was 64065f4)
Deleted tag 'bin-20190208-221206-814cb03' (was 814cb03)
Deleted tag 'bin-20190208-222309-650237b' (was 650237b)
Deleted tag 'bin-20190208-235057-8b51017' (was 8b51017)
Deleted tag 'bin-20190209-020632-22c7179' (was 22c7179)
Deleted tag 'bin-20190209-162751-484d864' (was 484d864)
Deleted tag 'bin-20190209-163013-088f753' (was 088f753)
Deleted tag 'bin-20190210-113848-ed4c536' (was ed4c536)
Deleted tag 'bin-20190210-131553-d6f84da' (was d6f84da)
Deleted tag 'bin-20190210-152455-c25122b' (was c25122b)
Deleted tag 'bin-20190210-171431-9b28db0' (was 9b28db0)
Deleted tag 'untagged-9164526c5fa59e86918d' (was e01e4d8)
buzzard@bob:~/Lean/lean-projects/mathlib-community-master$ git tag
buzzard@bob:~/Lean/lean-projects/mathlib-community-master$ git fetch
From github.com:leanprover-community/mathlib
 * [new tag]         bin-20190208-212100-4227f5c -> bin-20190208-212100-4227f5c
 * [new tag]         bin-20190208-220606-64065f4 -> bin-20190208-220606-64065f4
 * [new tag]         bin-20190208-221206-814cb03 -> bin-20190208-221206-814cb03
 * [new tag]         bin-20190208-222309-650237b -> bin-20190208-222309-650237b
 * [new tag]         bin-20190208-235057-8b51017 -> bin-20190208-235057-8b51017
 * [new tag]         bin-20190209-020632-22c7179 -> bin-20190209-020632-22c7179
 * [new tag]         bin-20190209-162751-484d864 -> bin-20190209-162751-484d864
 * [new tag]         bin-20190209-163013-088f753 -> bin-20190209-163013-088f753
 * [new tag]         bin-20190210-113848-ed4c536 -> bin-20190210-113848-ed4c536
 * [new tag]         bin-20190210-131553-d6f84da -> bin-20190210-131553-d6f84da
 * [new tag]         bin-20190210-152455-c25122b -> bin-20190210-152455-c25122b
 * [new tag]         bin-20190210-171431-9b28db0 -> bin-20190210-171431-9b28db0
 * [new tag]         untagged-9164526c5fa59e86918d -> untagged-9164526c5fa59e86918d
buzzard@bob:~/Lean/lean-projects/mathlib-community-master$ git tag
bin-20190208-212100-4227f5c
bin-20190208-220606-64065f4
bin-20190208-221206-814cb03
bin-20190208-222309-650237b
bin-20190208-235057-8b51017
bin-20190209-020632-22c7179
bin-20190209-162751-484d864
bin-20190209-163013-088f753
bin-20190210-113848-ed4c536
bin-20190210-131553-d6f84da
bin-20190210-152455-c25122b
bin-20190210-171431-9b28db0
untagged-9164526c5fa59e86918d
buzzard@bob:~/Lean/lean-projects/mathlib-community-master$

[Kevin Buzzard]

the tags have returned!

we don't need to change anything here (except we need people to stop pushing outdated tags)

Am I about to push an outdated tag?

[Chris Hughes]

What is a tag?

[Kevin Buzzard]

They're the things which completely screw you up when you do leanpkg upgrade and make you downgrade instead.

[Kevin Buzzard]

If your local copy of mathlib has a lean-3.4.2 tag then the next time you push it will be back, and then any time I type leanpkg upgrade ever I will end up at the commit which that tag points to.

[Chris Hughes]

Do I need to worry about this?

[Kevin Buzzard]

I think that the fact that one of my tags was lean-3.4.2 was somehow a bad thing.

[Kevin Buzzard]

This tag was created a while ago, and then when we pull we get it too, and then they remove it, but then when we push we put it back, and it messes things up.

[Kevin Buzzard]

if you have a command line handy you could try git tag -d lean-3.4.2

[Kevin Buzzard]

or you could type git tag first to see if you have one

[Kevin Buzzard]

somewhere in your mathlib repo