Zulip Chat Archive

Stream: general

Topic: AFP


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 07 2019 at 16:01):

PS thanks @Kenny Lau :-)

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 07 2019 at 22:48):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 07:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Feb 08 2019 at 07:42):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 23:08):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 08 2019 at 23:25):

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

view this post on Zulip Mario Carneiro (Feb 08 2019 at 23:25):

it's leanpkg, which is in core

view this post on Zulip Scott Morrison (Feb 08 2019 at 23:25):

Ah, of course.

view this post on Zulip 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"?

view this post 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Feb 08 2019 at 23:38):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Feb 09 2019 at 18:18):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:14):

so where are the compiled mathlibs now?

view this post on Zulip Chris Hughes (Feb 12 2019 at 13:15):

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

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:15):

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

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:15):

where are you?

view this post on Zulip Chris Hughes (Feb 12 2019 at 13:16):

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

view this post on Zulip Kenny Lau (Feb 12 2019 at 13:34):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:05):

What is the current status of precompiled mathlib?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:08):

So it's working well already?

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:08):

@Simon Hudon merci beaucoup pour le projet

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:09):

Vous êtes les bienvenus :)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:09):

But for some reason I can no longer find them

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:11):

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

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:12):

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

view this post on Zulip Reid Barton (Feb 12 2019 at 20:12):

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

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:14):

Are the releases on that branch still triggering emails?

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:15):

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

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:15):

They should not be

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Feb 12 2019 at 20:16):

That's true

view this post on Zulip Kenny Lau (Feb 12 2019 at 20:16):

I'm definitely for one release every commit

view this post on Zulip 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

view this post on Zulip Reid Barton (Feb 12 2019 at 20:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 12 2019 at 21:52):

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

view this post on Zulip Simon Hudon (Feb 12 2019 at 21:52):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 21:53):

bleeding edge isn't a tag

view this post on Zulip Mario Carneiro (Feb 12 2019 at 21:53):

it's just master

view this post on Zulip Simon Hudon (Feb 12 2019 at 21:53):

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

view this post on Zulip Reid Barton (Feb 12 2019 at 21:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Feb 12 2019 at 22:00):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 12 2019 at 22:08):

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

view this post on Zulip Mario Carneiro (Feb 12 2019 at 23:00):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 13 2019 at 20:30):

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

view this post on Zulip Reid Barton (Feb 13 2019 at 20:58):

That is the intent, not fully implemented just yet.

view this post on Zulip Kenny Lau (Feb 16 2019 at 14:40):

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

view this post on Zulip Simon Hudon (Feb 16 2019 at 21:34):

Why do you think that?

view this post on Zulip Kenny Lau (Feb 16 2019 at 21:36):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Feb 16 2019 at 21:48):

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

view this post on Zulip Simon Hudon (Feb 16 2019 at 22:06):

Right, that intent has yet to be implemented

view this post on Zulip Kenny Lau (Feb 20 2019 at 10:06):

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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Feb 20 2019 at 16:25):

I haven't gotten started yet

view this post on Zulip 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