AFP

Stream: general

[Sebastien Gouezel]

I am starting to submit more specialized material (Hausdorff distance in #PR696, but I have the Gromov-Hausdorff space waiting). While the Hausdorff distance is still of very broad use, I have the feeling that maybe the Gromov-Hausdorff space is too specialized for mathlib.

[Sebastien Gouezel]

In Isabelle, there is the AFP (archive of formal proof), containing formal developments that are too specialized for the main library. The point is that the maintainers of the main library also correct the AFP to make sure everything compiles all the time, avoiding bitrot. But someone who uses only the main library will not need to compile all of the AFP.

[Sebastien Gouezel]

I don't know anything about travis, but would it be easy to set up something similar for mathlib, i.e., parallel to src there would be a directory lafp or whatever name you like, that would not be compiled by lean --make by default but that would still be checked by travis?

[Kevin Buzzard]

I have often wondered what will become of the schemes and perfectoid projects. I forgot about schemes for months after I did it and turned my attention to perfectoid spaces, and then when I went back to it it was unsurprisingly very broken, because algebra had changed a lot, and I needed to get Kenny in to fix it. I feel like if I'd been notified the day a commit broke my repo it would have been a much less daunting job to fix it. Of course I can say "oh, it compiles with mathlib version x so use that" but I don't think that's a very good answer for something like perfectoid spaces -- people might want to use them for other things later as our ambitions grow, and incompatible software is probably a nightmare.

[Kevin Buzzard]

PS thanks @Kenny Lau :-)

[Simon Hudon]

The easiest way for the maintainers to ensure that it build with mathlib is to put it in mathlib itself. As for limiting compilation and recompilation, it certainly is an issue but I think right now it's better to address it by other means than cutting up mathlib in a myriad of small pieces.

[Scott Morrison]

I think it's important that maintaining compatibility becomes a broadly distributed obligation. We don't want this to start to fall on a "core" group of sacrificial maintainers. (As, perhaps, has happened with Isabelle.)

[Mario Carneiro]

I think it is important to maintain high standards for PR acceptance to prevent this kind of degradation

[Mario Carneiro]

what I think is a really bad idea is to have a bunch of "articles" that are owned by their authors and only subject to minor revision

[Mario Carneiro]

because this ties peoples' hands later when they want to generalize this or that

[Mario Carneiro]

As a PR author, you should not get too attached to your particular proofs or the way you structure a development - everything may be subject to change in the future at the behest of the maintainers or as a result of future PRs

[Chris Hughes]

I think it's important that maintaining compatibility becomes a broadly distributed obligation. We don't want this to start to fall on a "core" group of sacrificial maintainers. (As, perhaps, has happened with Isabelle.)

I guess putting everything all together puts the burden of maintenance on whoever makes a PR that breaks everything.

[Mario Carneiro]

The only thing I would try to maintain is monotonicity with respect to proven theorems, i.e. if you prove Sylow's theorem then you can be sure that all future versions of mathlib will have Sylow's theorem, although the proof might change completely, the statement might change, the file could move, etc. (Your name will remain attached to any future versions though)

[Sebastien Gouezel]

I guess putting everything all together puts the burden of maintenance on whoever makes a PR that breaks everything.

For instance, if someone changes the name of a lemma in mathlib for better coherence, then she should change the name of all applications of this lemma in mathlib, but also in the AFP. That sounds reasonable, since she knows exactly which lemmas can break, and the new names. On the other hand, the author of the AFP entry is not aware of the name change, he will only see that the old name does not work anymore, but he will have no clue on the new name and it will take much longer for him to find the new name.

[Sebastien Gouezel]

To be sure that this is the job of the PR author and not of the maintainer, it is enough that the green light on travis indicates that both mathlib and AFP compile correctly together.

[Mario Carneiro]

I don't really see what the benefit is of a quarantine like this for some part of mathlib

[Mario Carneiro]

so what if it's specialized? I think that we should focus more on being able to make use of mathlib where only half of it is compiled because you don't care about the rest

[Johan Commelin]

That would be cool, I'm perfectly able to use half of a math book and not care about the rest. Lean should be able to do that to.

[Mario Carneiro]

I mean lean can do this now. It's just a question of what to lean --make

[Mario Carneiro]

But it's simpler and easier to just compile everything when in doubt currently

[Mario Carneiro]

I am not sure if lean --make foo.lean will compile all and only the dependencies of foo, but if so then if foo is your project then you can just make sure that all the theories you care about are imported, then compile it

[Mario Carneiro]

One option is to have a generalization of init.default import lists, where we have a curated collection of big theory imports. So for example "core only", "mathlib tactics", "programming tools", "basic natural numbers", "commutative algebra", "analysis and measure theory", "computability", "everything" etc. You load one of these files and they import a relatively complete list of files useful for the target area. That way if you care about analysis and measure theory you just lean --make this file, import it, and you are all set

[Mario Carneiro]

One of these lists can be a rough analogue of what Isabelle calls the standard library (as distinct from the AFP). Anything not in that list is "more specialized" and probably isn't useful for people who just say "I want mathlib"

[Mario Carneiro]

(Note, these would not be used inside mathlib itself, which needs more fine grained dependency tracking)

[Johan Commelin]

But a helper tool could explode the import init.big.list into import fine.grained dep.end.encies.

[Mario Carneiro]

sure... couple that with import analysis and it could be a quick post processing step on PRs

[Sebastien Gouezel]

I agree that having different make targets (and being able to lean --make foo.lean) would be a perfect solution.

[Simon Hudon]

This discussion has inspired me to write a tool which I have just pushed to master. When you import mathlib, you shouldn't have to build any of it yourself anymore. The instructions on installing the tool are in mathlib's readme file

[Mario Carneiro]

You should describe the tool here on zulip too - what's it good for, how is it used

[Mario Carneiro]

also that sounds suspiciously like something that should have gone through a PR process first :P

[Simon Hudon]

The PR didn’t get much attention so I thought I’d release it to get feedback from users. Maybe I should have tried louder advertisements

[Simon Hudon]

The script, when you call it, checks which version of mathlib your project uses and fetches olean files for it. You can also set it up to get called every time you check out a branch

[Simon Hudon]

If I could get elan to call it too after leanpkg configure you should never have to compile mathlib except when you’re developing mathlib

[Mario Carneiro]

The PR didn’t get much attention so I thought I’d release it

Hm, this seems like a bad default

[Scott Morrison]

What's the obstacle to having leanpkg configure call it.

[Mario Carneiro]

it's leanpkg, which is in core

[Scott Morrison]

Ah, of course.

[Scott Morrison]

Regarding the PR process --- perhaps we can ask everyone to add the extra step "if you've asked for reviewers, and not got any after a reasonable amount of time, you can ask plaintively on the PR reviews stream on zulip"?

[Mario Carneiro]

I think the build instructions should be moved off the main readme, they can be in a separate file linked from the readme

[Simon Hudon]

I think compilation is a major part of using mathlib. I think it should be available as one of the first things you read about mathlib

[Simon Hudon]

@Scott Morrison I think you're right. In any case, I might have been overly eager to deploy.

[Chris Hughes]

Can I use update-mathlib if I just git clone the repository without using adding it as a dependency to a project using leanpkg?

[Simon Hudon]

Meaning that you want to work on mathlib itself and you want to get started with a fully compiled set of olean files? update-mathlib does not handle that as of yet. I can look into making that work.

[Simon Hudon]

How do you feel about calling it as update-mathlib here?

[Johan Commelin]

One downside of this change is that my github inbox is now being spammed with new tags that are created. Does anyone know how I can mute those? I appreciate only seeing PRs and other issues in that inbox.

[Gabriel Ebner]

@Simon Hudon Can you maybe push these binaries to a different repository instead? Kind of like leanprover/lean vs. leanprover/lean-nightly. Johan is not the only one who's annoyed by the spammy emails. It also clutters the tig output.

[Simon Hudon]

Sure, I'll get right on it. What is the tig output?

[Simon Hudon]

@Gabriel Ebner Is there a way to get Travis to upload a release to a separate repository?

[Kenny Lau]

so where are the compiled mathlibs now?

[Chris Hughes]

https://github.com/leanprover-community/mathlib-nightly/releases

[Patrick Massot]

But the update-mathlib script doesn't seem to work

[Kenny Lau]

where are you?

[Chris Hughes]

I couldn't get update-mathlib to work either.

[Kenny Lau]

and also I can't find the version of the nightly

[Kenny Lau]

also now that the builds are not clogging up people's emails, could we revert back to building it every commit?

[Kenny Lau]

The releases were the best thing that happened to be this month, many thanks for whoever was behind it; I absolutely did not mind my emails being clogged in exchange for a precompiled up-to-date mathlib

[Kenny Lau]

What is the current status of precompiled mathlib?

[Kevin Buzzard]

@Simon Hudon I told you in private that this .olean project was a game-changer for some of my students, and there you have first hand proof.

[Simon Hudon]

So it's working well already?

[Kenny Lau]

@Simon Hudon merci beaucoup pour le projet

[Simon Hudon]

Vous êtes les bienvenus :)

[Kenny Lau]

It was working well, in the sense that whenever mathlib changes I could find the corresponding precompiled version at https://github.com/leanprover-community/mathlib/releases

[Kenny Lau]

But for some reason I can no longer find them

[Simon Hudon]

Right, we're making a lot of changes. We moved the binaries to leanprover-community/mathlib-nightly

[Kenny Lau]

however that branch is configured to release once every day instead of once every mathlib commit

[Simon Hudon]

That's right, people were complaining that there were too many releases

[Reid Barton]

I think people were actually complaining about too many emails :upside_down:

[Kenny Lau]

Are the releases on that branch still triggering emails?

[Simon Hudon]

Indeed! Is there a need for that many releases by the way?

[Simon Hudon]

They should not be

[Reid Barton]

It might be nice to have a shorter turn-around time for people who are moving bits of their projects into mathlib, I guess?

[Simon Hudon]

That's true

[Kenny Lau]

I'm definitely for one release every commit

[Simon Hudon]

Ok, so we can move lean-3.4.2 once a day and produce one binary per commit

[Reid Barton]

why not just move lean-3.4.2 on every commit as well?

[Simon Hudon]

To give it some stability. If you want to be bleeding edge, you'll have to copy the commit hashes. Otherwise, people who upgrade their dependency on mathlib on the same day will agree on which version to use

[Mario Carneiro]

I would like a way to be bleeding edge without having to change a value every commit

[Mario Carneiro]

also my original proposal for binary releases would have one bleeding edge release plus a nightly breadcrumb

[Simon Hudon]

Do you think that having lean-3.4.2 be almost a synonym of master would be the way to go?

[Mario Carneiro]

no, I think master = bleeding edge and lean-3.4.2 = stable-ish seems good

[Simon Hudon]

Do you want a lean-3.4.2 tag and a bleeding-edge tag?

[Mario Carneiro]

bleeding edge isn't a tag

[Mario Carneiro]

it's just master

[Simon Hudon]

How do you get leanpkg upgrade to fetch master instead of lean-3.4.2?

[Reid Barton]

you can't, currently
This is why #365 is an issue

[Reid Barton]

At one point, our goal was to just make lean-3.4.2 stay equal to master

[Reid Barton]

so basically, there's the fixed name lean-3.4.2 which leanpkg will fetch, and we need to decide how we want it to behave

[Simon Hudon]

The down side of working off of master btw is that sometimes, the build breaks

[Kevin Buzzard]

When Mario and Johannes were the only people who could push to master it was extremely rare that master didn't compile

[Patrick Massot]

We could still have a stable branch that would be pushed only manually

[Mario Carneiro]

Actually, that seems like something we could fold into the travis build

[Mario Carneiro]

if the build of master fails, we don't push binaries and don't update lean-3.4.2, otherwise we update it to the latest

[Kenny Lau]

So is there a precompiled mathlib for every (successfully built) commit?

[Reid Barton]

That is the intent, not fully implemented just yet.

[Kenny Lau]

https://github.com/leanprover-community/mathlib-nightly/releases is frozen again?

[Simon Hudon]

Why do you think that?

[Kenny Lau]

because the last commit for Feb 15 is 8730619 instead of 17f9bef

[Simon Hudon]

There reason is that there's one nightly release per calendar day. 8730619 was pushed on the same day (according to GMT time) as 17f9bef.

[Kenny Lau]

and above Reid claims that the intent is one release per commit

[Simon Hudon]

Right, that intent has yet to be implemented

[Kenny Lau]

@Simon Hudon what's the progress of the implementation of the intent?

[Kenny Lau]

also shouldn't 78ce6e4 be released on Feb 19 despite there not being any commit on Feb 19?

[Simon Hudon]

I haven't gotten started yet

[Simon Hudon]

also shouldn't 78ce6e4 be released on Feb 19 despite there not being any commit on Feb 19?

No, the way it works is that it takes the first successful commit of the day as the nightly for that day