lean-3.4.1 branch

Stream: general

[Mario Carneiro]

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]

Mario -- many thanks!

[Kevin Buzzard]

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]

Why not just have a release version for 3.4.1?

[Mario Carneiro]

because lean does not have nearly enough versions

[Mario Carneiro]

mathlib does not develop on lean's schedule

[Mario Carneiro]

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

[Kevin Buzzard]

I understand the argument.

[Kevin Buzzard]

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]

And your argument is

[Kevin Buzzard]

that the canonical version is the latest version

[Kevin Buzzard]

right?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

The problem with that idea

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

Oh -- so 3.3.0 moves?

[Patrick Massot]

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

[Kevin Buzzard]

Oh!

[Mario Carneiro]

not much, but yes

[Patrick Massot]

You can tag a commit

[Kevin Buzzard]

Aah

[Kevin Buzzard]

Mario -- last question then

[Kevin Buzzard]

can I persuade you to tag a commit?

[Patrick Massot]

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

[Patrick Massot]

What you want is Mario creating a release tag

[Patrick Massot]

not a branch

[Kevin Buzzard]

Thanks for clarifying Patrick.

[Mario Carneiro]

mathlib doesn't do releases like that

[Kevin Buzzard]

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

[Patrick Massot]

Kevin kindly asks to change this

[Mario Carneiro]

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]

I can do this

[Kevin Buzzard]

but it will look confusing

[Kevin Buzzard]

I am not asking for this for me

[Kevin Buzzard]

I am asking for this for other people

[Kevin Buzzard]

who want "Lean + Mathlib version 3.4.1"

[Mario Carneiro]

That's what the branch is for

[Kevin Buzzard]

no

[Kevin Buzzard]

They want a canonical uniquely defined thing

[Kevin Buzzard]

not a moving target

[Kevin Buzzard]

because both refuse to move

[Kevin Buzzard]

I will give them a hash

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

because I want leanpkg to find the branch

[Kevin Buzzard]

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

[Patrick Massot]

I don't understand the potential problem here

[Patrick Massot]

with a tagged release

[Johan Commelin]

Just don't tag it with lean-3.4.1

[Mario Carneiro]

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]

Right, Kevin, maybe you can trick them.

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Patrick Massot]

Just don't tag it with lean-3.4.1

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

We probably need to wait for @Sebastian Ullrich then

[Patrick Massot]

oops

[Patrick Massot]

We pinged him at the same time

[Patrick Massot]

sorry about the harassment

[Johan Commelin]

Urgent matters (-;

[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.

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]

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

[Sebastian Ullrich]

Uh, where?

[Mario Carneiro]

leanpkg.toml

[Mario Carneiro]

lean_version = "3.4.1"

[Sebastian Ullrich]

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]

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]

Is there any Lean nightly though?

[Mario Carneiro]

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

[Sebastian Ullrich]

Yes, both ways should work fine

[Sebastian Ullrich]

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