## Stream: general

### Topic: AFP

#### Sebastien Gouezel (Feb 07 2019 at 14:37):

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 (Feb 07 2019 at 14:40):

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 (Feb 07 2019 at 14:41):

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 (Feb 07 2019 at 16:01):

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 (Feb 07 2019 at 16:01):

PS thanks @Kenny Lau :-)

#### Simon Hudon (Feb 07 2019 at 19:02):

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 (Feb 07 2019 at 22:44):

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 (Feb 07 2019 at 22:47):

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

#### Mario Carneiro (Feb 07 2019 at 22:48):

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 (Feb 07 2019 at 22:48):

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

#### Mario Carneiro (Feb 07 2019 at 22:50):

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 (Feb 07 2019 at 22:50):

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 (Feb 07 2019 at 22:51):

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 (Feb 08 2019 at 07:25):

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 (Feb 08 2019 at 07:27):

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 (Feb 08 2019 at 07:29):

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

#### Mario Carneiro (Feb 08 2019 at 07:30):

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 (Feb 08 2019 at 07:30):

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 (Feb 08 2019 at 07:31):

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

#### Mario Carneiro (Feb 08 2019 at 07:31):

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

#### Mario Carneiro (Feb 08 2019 at 07:33):

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 (Feb 08 2019 at 07:39):

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 (Feb 08 2019 at 07:41):

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 (Feb 08 2019 at 07:42):

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

#### Johan Commelin (Feb 08 2019 at 07:44):

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

#### Mario Carneiro (Feb 08 2019 at 07:44):

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

#### Sebastien Gouezel (Feb 08 2019 at 08:30):

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

#### Simon Hudon (Feb 08 2019 at 22:49):

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 (Feb 08 2019 at 23:07):

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

#### Mario Carneiro (Feb 08 2019 at 23:08):

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

#### Simon Hudon (Feb 08 2019 at 23:20):

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 (Feb 08 2019 at 23:22):

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 (Feb 08 2019 at 23:24):

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 (Feb 08 2019 at 23:24):

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

Hm, this seems like a bad default

#### Scott Morrison (Feb 08 2019 at 23:25):

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

#### Mario Carneiro (Feb 08 2019 at 23:25):

it's leanpkg, which is in core

Ah, of course.

#### Scott Morrison (Feb 08 2019 at 23:26):

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 (Feb 08 2019 at 23:27):

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 (Feb 08 2019 at 23:31):

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 (Feb 08 2019 at 23:33):

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

#### Chris Hughes (Feb 08 2019 at 23:35):

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 (Feb 08 2019 at 23:38):

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 (Feb 08 2019 at 23:38):

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

#### Johan Commelin (Feb 09 2019 at 07:03):

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 (Feb 09 2019 at 14:35):

@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 (Feb 09 2019 at 18:18):

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

#### Simon Hudon (Feb 09 2019 at 18:55):

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

#### Kenny Lau (Feb 12 2019 at 13:14):

so where are the compiled mathlibs now?

#### Chris Hughes (Feb 12 2019 at 13:15):

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

#### Patrick Massot (Feb 12 2019 at 13:15):

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

where are you?

#### Chris Hughes (Feb 12 2019 at 13:16):

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

#### Kenny Lau (Feb 12 2019 at 13:34):

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

#### Kenny Lau (Feb 12 2019 at 19:48):

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

#### Kenny Lau (Feb 12 2019 at 20:04):

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 (Feb 12 2019 at 20:05):

What is the current status of precompiled mathlib?

#### Kevin Buzzard (Feb 12 2019 at 20:07):

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

#### Kenny Lau (Feb 12 2019 at 20:08):

@Simon Hudon merci beaucoup pour le projet

#### Simon Hudon (Feb 12 2019 at 20:09):

Vous êtes les bienvenus :)

#### Kenny Lau (Feb 12 2019 at 20:09):

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 (Feb 12 2019 at 20:09):

But for some reason I can no longer find them

#### Simon Hudon (Feb 12 2019 at 20:10):

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

#### Kenny Lau (Feb 12 2019 at 20:11):

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

#### Simon Hudon (Feb 12 2019 at 20:12):

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

#### Reid Barton (Feb 12 2019 at 20:12):

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

#### Kenny Lau (Feb 12 2019 at 20:14):

Are the releases on that branch still triggering emails?

#### Simon Hudon (Feb 12 2019 at 20:15):

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

#### Simon Hudon (Feb 12 2019 at 20:15):

They should not be

#### Reid Barton (Feb 12 2019 at 20:15):

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

That's true

#### Kenny Lau (Feb 12 2019 at 20:16):

I'm definitely for one release every commit

#### Simon Hudon (Feb 12 2019 at 20:17):

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

#### Reid Barton (Feb 12 2019 at 20:31):

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

#### Simon Hudon (Feb 12 2019 at 20:36):

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 (Feb 12 2019 at 21:50):

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

#### Mario Carneiro (Feb 12 2019 at 21:52):

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

#### Simon Hudon (Feb 12 2019 at 21:52):

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

#### Mario Carneiro (Feb 12 2019 at 21:52):

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

#### Simon Hudon (Feb 12 2019 at 21:52):

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

#### Mario Carneiro (Feb 12 2019 at 21:53):

bleeding edge isn't a tag

#### Mario Carneiro (Feb 12 2019 at 21:53):

it's just master

#### Simon Hudon (Feb 12 2019 at 21:53):

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

#### Reid Barton (Feb 12 2019 at 21:54):

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

#### Reid Barton (Feb 12 2019 at 21:57):

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

#### Reid Barton (Feb 12 2019 at 22:00):

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 (Feb 12 2019 at 22:00):

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

#### Kevin Buzzard (Feb 12 2019 at 22:07):

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

#### Patrick Massot (Feb 12 2019 at 22:08):

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

#### Mario Carneiro (Feb 12 2019 at 23:00):

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

#### Mario Carneiro (Feb 12 2019 at 23:01):

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 (Feb 13 2019 at 20:30):

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

#### Reid Barton (Feb 13 2019 at 20:58):

That is the intent, not fully implemented just yet.

#### Kenny Lau (Feb 16 2019 at 14:40):

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

#### Simon Hudon (Feb 16 2019 at 21:34):

Why do you think that?

#### Kenny Lau (Feb 16 2019 at 21:36):

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

#### Simon Hudon (Feb 16 2019 at 21:47):

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 (Feb 16 2019 at 21:48):

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

#### Simon Hudon (Feb 16 2019 at 22:06):

Right, that intent has yet to be implemented

#### Kenny Lau (Feb 20 2019 at 10:06):

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

#### Kenny Lau (Feb 20 2019 at 10:07):

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

#### Simon Hudon (Feb 20 2019 at 16:25):

I haven't gotten started yet

#### Simon Hudon (Feb 20 2019 at 16:30):

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

Last updated: May 13 2021 at 21:12 UTC