Zulip Chat Archive

Stream: general

Topic: lean-3.4.1 branch


Mario Carneiro (May 25 2018 at 10:00):

I added a lean-3.4.1 branch to mathlib, which I think should fix the issues with elan/leanpkg (assuming I spelled everything correctly). @Sebastian Ullrich Will there be any problem with just keeping the branch up to date with master (although I don't think branch symlinks are a thing)? I don't see any reason not to.

Kevin Buzzard (May 25 2018 at 10:01):

Mario -- many thanks!

Kevin Buzzard (May 25 2018 at 10:02):

You did not keep the 3.3.0 branch up to date with mathlib master -- why do you want to keep the 3.4.1 branch up to date?

Kevin Buzzard (May 25 2018 at 10:02):

Why not just have a release version for 3.4.1?

Mario Carneiro (May 25 2018 at 10:06):

because lean does not have nearly enough versions

Mario Carneiro (May 25 2018 at 10:07):

mathlib does not develop on lean's schedule

Mario Carneiro (May 25 2018 at 10:07):

and there is a huge range of commits that are compatible with 3.4.1

Kevin Buzzard (May 25 2018 at 10:08):

I understand the argument.

Kevin Buzzard (May 25 2018 at 10:09):

As I explained to you in email -- I would ideally like to be able to point people to a "3.4.1 release" version of mathlib which is "the canonical version of mathlib to run with the 3.4.1 release version of Lean"

Kevin Buzzard (May 25 2018 at 10:09):

And your argument is

Kevin Buzzard (May 25 2018 at 10:09):

that the canonical version is the latest version

Kevin Buzzard (May 25 2018 at 10:09):

right?

Kevin Buzzard (May 25 2018 at 10:10):

OTOH I am _forced_ to point certain people (the IT people here, the CoCalc people) to a canonical version of mathlib which goes with Lean 3.4.1 release, because both of these organisations refuse to work with moving targets

Kevin Buzzard (May 25 2018 at 10:10):

so I am going to tell them both to point to the very first commit in the 3.4.1 branch.

Kevin Buzzard (May 25 2018 at 10:10):

I cannot envisage any problems with this, and it sounds like the best compromise.

Mario Carneiro (May 25 2018 at 10:11):

You can point them to the latest version, and they can take that at any point

Kevin Buzzard (May 25 2018 at 10:11):

The problem with that idea

Kevin Buzzard (May 25 2018 at 10:11):

is that then it will be hard for people to work out exactly which version they are running

Kevin Buzzard (May 25 2018 at 10:11):

and it is very much in my interest that code runs on CoCalc if and only if it runs on the machines here

Kevin Buzzard (May 25 2018 at 10:12):

so I would very much like CoCalc and the machines here to be running exactly the same code

Mario Carneiro (May 25 2018 at 10:12):

We have a lean-3.3.0 branch as well, which is not a tag but a branch because it incorporates new bugfixes and such which are compatible with 3.3.0

Kevin Buzzard (May 25 2018 at 10:12):

Oh -- so 3.3.0 moves?

Patrick Massot (May 25 2018 at 10:12):

There nothing like "the very first commit in the 3.4.1 branch" in git

Kevin Buzzard (May 25 2018 at 10:12):

Oh!

Mario Carneiro (May 25 2018 at 10:12):

not much, but yes

Patrick Massot (May 25 2018 at 10:12):

You can tag a commit

Kevin Buzzard (May 25 2018 at 10:12):

Aah

Kevin Buzzard (May 25 2018 at 10:12):

Mario -- last question then

Kevin Buzzard (May 25 2018 at 10:13):

can I persuade you to tag a commit?

Patrick Massot (May 25 2018 at 10:13):

But a branch is only some moving marker attached to some moving commit

Patrick Massot (May 25 2018 at 10:13):

What you want is Mario creating a release tag

Patrick Massot (May 25 2018 at 10:13):

not a branch

Kevin Buzzard (May 25 2018 at 10:14):

Thanks for clarifying Patrick.

Mario Carneiro (May 25 2018 at 10:14):

mathlib doesn't do releases like that

Kevin Buzzard (May 25 2018 at 10:14):

Sorry that my poor understanding of git is just adding to the noise

Patrick Massot (May 25 2018 at 10:14):

Kevin kindly asks to change this

Mario Carneiro (May 25 2018 at 10:14):

if you want a commit, then it will be an artificial stopping point anyway, so just pick a point and write down the hash

Kevin Buzzard (May 25 2018 at 10:14):

I can do this

Kevin Buzzard (May 25 2018 at 10:14):

but it will look confusing

Kevin Buzzard (May 25 2018 at 10:15):

I am not asking for this for me

Kevin Buzzard (May 25 2018 at 10:15):

I am asking for this for other people

Kevin Buzzard (May 25 2018 at 10:15):

who want "Lean + Mathlib version 3.4.1"

Mario Carneiro (May 25 2018 at 10:15):

That's what the branch is for

Kevin Buzzard (May 25 2018 at 10:15):

no

Kevin Buzzard (May 25 2018 at 10:15):

They want a canonical uniquely defined thing

Kevin Buzzard (May 25 2018 at 10:15):

not a moving target

Kevin Buzzard (May 25 2018 at 10:15):

because both refuse to move

Kevin Buzzard (May 25 2018 at 10:16):

I will give them a hash

Kevin Buzzard (May 25 2018 at 10:16):

It is not ideal, but it is the best solution if there is to be no release tag

Kevin Buzzard (May 25 2018 at 10:17):

Thanks both of you for clarifying what I should be doing :-)

Mario Carneiro (May 25 2018 at 10:17):

I think 78d28c5cb58f6a22fbb8fc940cc6f97bc0111602 is the last "update to lean" commit

Mario Carneiro (May 25 2018 at 10:18):

but I don't know what leanpkg does with tags v branches, so I don't want to carelessly tag it

Mario Carneiro (May 25 2018 at 10:18):

because I want leanpkg to find the branch

Kevin Buzzard (May 25 2018 at 10:19):

If creating a tag causes problems for other people then clearly this is an argument against creating a tag

Patrick Massot (May 25 2018 at 10:19):

I don't understand the potential problem here

Patrick Massot (May 25 2018 at 10:19):

with a tagged release

Johan Commelin (May 25 2018 at 10:20):

Just don't tag it with lean-3.4.1

Mario Carneiro (May 25 2018 at 10:20):

if you ask for elan to give you lean + mathlib 3.4.1, you should get the latest mathlib that is compatible with 3.4.1, which is master

Johan Commelin (May 25 2018 at 10:20):

Right, Kevin, maybe you can trick them.

Johan Commelin (May 25 2018 at 10:21):

You ask them to install elan, and use elan to install mathlib 3.4.1

Johan Commelin (May 25 2018 at 10:21):

And they won't realise they just installed a moving target...

Mario Carneiro (May 25 2018 at 10:22):

that's what travis did for a long time, and it worked pretty well

Patrick Massot (May 25 2018 at 10:22):

Just don't tag it with lean-3.4.1

Sure, the tag would need to be something like: spring2018

Johan Commelin (May 25 2018 at 10:22):

Otoh, if users start complaining, you're in trouble anyway...

Johan Commelin (May 25 2018 at 10:22):

Because they will say: hey, why is this stuff not in your mathlib...

Mario Carneiro (May 25 2018 at 10:23):

I don't mind having mathlib versions (which would be different from lean versions), but I would like leanpkg to work with them if possible

Johan Commelin (May 25 2018 at 10:23):

Right, so @Sebastian Ullrich can you make elan to listen to some tags as well?

Patrick Massot (May 25 2018 at 10:23):

We probably need to wait for @Sebastian Ullrich then

Patrick Massot (May 25 2018 at 10:23):

oops

Patrick Massot (May 25 2018 at 10:23):

We pinged him at the same time

Patrick Massot (May 25 2018 at 10:24):

sorry about the harassment

Johan Commelin (May 25 2018 at 10:24):

Urgent matters (-;

Sebastian Ullrich (May 25 2018 at 10:49):

Will there be any problem with just keeping the branch up to date with master (although I don't think branch symlinks are a thing)? I don't see any reason not to.

Yes, I think it's either that or saying "Nobody should use nightlies right now anyway", setting lean-3.4.1 as the default branch, and not updating or outright removing master

Mario Carneiro (May 25 2018 at 10:49):

I did set the mathlib dependency to lean-3.4.1 as well

Sebastian Ullrich (May 25 2018 at 10:50):

Uh, where?

Mario Carneiro (May 25 2018 at 10:50):

leanpkg.toml

Mario Carneiro (May 25 2018 at 10:51):

lean_version = "3.4.1"

Sebastian Ullrich (May 25 2018 at 10:54):

Ah, I see. Yeah, it's a bit weird to do that on the master branch since it means Lean nightly people using mathlib will get warnings, which is why I would slightly prefer the latter option I listed. But I guess it's okay either way.

Mario Carneiro (May 25 2018 at 10:55):

I mean, right now there's no difference, and it seems like lean repo is frozen for the foreseeable future so I guess it's fine to officially run 3.4.1

Patrick Massot (May 25 2018 at 10:55):

Is there any Lean nightly though?

Mario Carneiro (May 25 2018 at 10:56):

if and when nightlies start back up again we can switch back

Sebastian Ullrich (May 25 2018 at 10:56):

Yes, both ways should work fine

Sebastian Ullrich (May 25 2018 at 10:59):

As Mario said, tag support would have to be added to leanpkg, unless we'd want elan to more or less reimplement and supersede the former. Which is possibly, and https://github.com/Kha/elan/issues/7 already points in that direction, but... not something I want to do right now


Last updated: Dec 20 2023 at 11:08 UTC