Zulip Chat Archive

Stream: condensed mathematics

Topic: for_mathlib


view this post on Zulip Kevin Buzzard (Feb 05 2021 at 17:55):

OK so we're not quite at lean-perfectoid-space levels yet,but with 14 files in for_mathlib we are beginning to walk into the same trap which Johan, Patrick and I walked into in 2019, generating a whole bunch of stuff which was _clearly_ for mathlib, much of it even mathlib-ready, and then not PR'ing it and then it rotted and the work we put in there was, arguably, wasted (although of course it fulfilled the role of helping us formalise perfectoid spaces). Do we have a plan here, or are we just going to watch this directory fill up and then go "oh look it happened again"? There are over 1300 lines of code in that directory so far.

view this post on Zulip Patrick Massot (Feb 05 2021 at 17:57):

My opinion is we should explicitly state that everything in the folder can be PRed to mathlib by anyone. If it means someone feel they lose credit then it means they should have made the PRing effort. Of course when things do not get PRed then the author should still be the only one to feel bad.

view this post on Zulip Johan Commelin (Feb 05 2021 at 18:03):

yes, I very much agree with what Patrick said.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:03):

I personally never feel that it is about "credit". However when I was making the universal_universe branch on this repo I didn't put anything in for_mathlib, I just made notes of what needed to be PR'ed and am slowly PR'ing it myself. I did the same today. I think there is a risk that nobody does it. Of course anyone can feel free to do it, but we all know it's hard work. I am wondering if we need a better plan than this. Or do you think I'm overreacting and it doesn't matter?

Chris Hughes has long argued that free_abelian_group should be defined via finsupp. I see now that Johan has just made the interface relating the current definition to finsupp. Chris won't be happy because he wanted the equality to be definitional, but I am less excited by definitional equality than he is. This is 300 lines of code though. It probably should not be lost!

view this post on Zulip Johan Commelin (Feb 05 2021 at 18:10):

I agree that we should work on PRing things. But on the other hand, momentum is also a weird concept... once I have momentum working on a project like this, I just want to march forward, and not be blocked by PRs.

view this post on Zulip Johan Commelin (Feb 05 2021 at 18:10):

Something I would like to experiment with, is whether we can do some sort of for_mathlib PR sprints.

view this post on Zulip Johan Commelin (Feb 05 2021 at 18:11):

Once we reach some sort of intermediate milestone/target, we just take a step back, and create 37 PRs to mathlib. And after that we plunge forward to the next target.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:27):

Johan this is exactly how I felt with perfectoid. Once I could see that it was possible to do this kind of mathematics in Lean (because in 2018 this was not yet clear, as you well remember!), I would just throw myself into a lot of focussed coding with clear well-defined goals in mind and fill up for_mathlib and just not worry. All three of us were doing it, and then Patrick suddenly saw sense and PR'd a whole bunch of topology into mathlib (all the Bourbaki stuff which he'd done) -- but I can't remember whether this was during the sprint to the def or after we had the def.

view this post on Zulip Patrick Massot (Feb 05 2021 at 18:47):

It was during the sprint, but there was a special trick. mathlib had stuff about this, but it wasn't good enough and was actually getting in our way. That's why I was force to work on the mathlib side.

view this post on Zulip Scott Morrison (Feb 05 2021 at 22:29):

I'm glad there's consensus that "anyone should feel free to make the PRs from for_mathlib". This is a chore that I don't find particularly tedious, and will make some effort at it after the weekend!

view this post on Zulip Johan Commelin (Feb 10 2021 at 12:46):

Anyone looking for some PRs to make:

$ find src/for_mathlib/ -name '*.lean' | xargs wc -l
  189 src/for_mathlib/sequences.lean
   21 src/for_mathlib/category_theory.lean
   34 src/for_mathlib/tsum.lean
   31 src/for_mathlib/extend_from_nat.lean
  403 src/for_mathlib/normed_group_hom.lean
   55 src/for_mathlib/equalizers.lean
  114 src/for_mathlib/topology.lean
   18 src/for_mathlib/linear_algebra.lean
   19 src/for_mathlib/topological_group.lean
   62 src/for_mathlib/locally_constant.lean
  362 src/for_mathlib/free_abelian_group.lean
   40 src/for_mathlib/compact.lean
   92 src/for_mathlib/add_monoid_hom.lean
 1440 total

view this post on Zulip Johan Commelin (Feb 10 2021 at 12:47):

I think I'll take on free_abelian_group and locally_constant

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 12:50):

I can do sequences

view this post on Zulip Riccardo Brasca (Feb 10 2021 at 12:55):

Ops, it depends on locally_constant, it is better to wait.

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 13:52):

I made a PR to free_abelian_group recently, which came out of the universal maps stuff. #6062. It's waiting for epsilon more work by me.

view this post on Zulip Johan Commelin (Feb 10 2021 at 21:37):

I ended up working on for_mathlib/compact first...

view this post on Zulip Johan Commelin (Feb 10 2021 at 21:37):

I hope to tackle locally_constant asap

view this post on Zulip Johan Commelin (Feb 11 2021 at 21:47):

for_mathlib/locally_constant has now been PRd

view this post on Zulip Johan Commelin (Feb 23 2021 at 08:45):

#6375 PRs most of normed_group_hom to mathlib. About 20% of for_mathlib (-;

view this post on Zulip Johan Commelin (Mar 10 2021 at 06:38):

This PR has now been merged, and so ~370 lines of for_mathlib were deleted this morning.

view this post on Zulip Johan Commelin (Mar 10 2021 at 06:38):

Be sure to git pull before you work on master

view this post on Zulip Johan Commelin (Mar 10 2021 at 06:39):

What is left:

  185 src/for_mathlib/sequences.lean
   34 src/for_mathlib/tsum.lean
   31 src/for_mathlib/extend_from_nat.lean
   55 src/for_mathlib/equalizers.lean
  114 src/for_mathlib/topology.lean
   14 src/for_mathlib/pi_nat_apply.lean
   18 src/for_mathlib/linear_algebra.lean
   19 src/for_mathlib/topological_group.lean
  362 src/for_mathlib/free_abelian_group.lean
  319 src/for_mathlib/normed_group_quotient.lean
   92 src/for_mathlib/add_monoid_hom.lean
 1243 total

Last updated: May 09 2021 at 22:13 UTC