Zulip Chat Archive

Stream: mathlib4

Topic: porting requests


Mario Carneiro (Oct 25 2022 at 20:39):

Since we have a wide open space of files to port at the moment, I thought I would make a thread for people to request specific files to get them bumped up in priority.

Mario Carneiro (Oct 25 2022 at 20:40):

  • algebra.invertible: I'm going to need parts of this for norm_num, although I can work around it for now.

Scott Morrison (Oct 25 2022 at 20:47):

For which

leanproject import-graph --to algebra.invertible --exclude-tactics --port-status algebra.invertible.pdf

says algebra.invertible.pdf.

Scott Morrison (Oct 25 2022 at 20:49):

This may be a case where refactoring the file in mathlib3 to isolate the parts you need might be warranted first.

Mario Carneiro (Oct 25 2022 at 21:02):

yikes

Scott Morrison (Oct 25 2022 at 21:04):

Yeah, import creep is vicious. :-)

Mario Carneiro (Oct 25 2022 at 21:04):

I remember the days when stuff in "algebra" was supposed to have low dependencies

Mario Carneiro (Oct 25 2022 at 21:04):

I think it was a poor choice of name

Scott Morrison (Oct 25 2022 at 21:05):

Most of this tree is transitive imports via algebra.order.ring and data.set.lattice. I suspect very large portions of algebra.invertible don't need anything from either of those.

Mario Carneiro (Oct 25 2022 at 21:07):

data.nat.cast -> algebra.ne_zero seems super suspicious

Eric Rodriguez (Oct 25 2022 at 21:09):

I thought I turned that inside out? I'm not sure what happened

Eric Rodriguez (Oct 25 2022 at 21:09):

maybe it was for add_monoid_with_one stuff

Eric Rodriguez (Oct 25 2022 at 21:10):

it used to import algebra.invertible before too :)

Mario Carneiro (Oct 25 2022 at 21:12):

I feel like we need a bot that posts about "dependency regressions" in mathlib similar to performance regressions in software projects. "The average number of transitive dependencies went up by 10 by this PR" would be nice to see

Ruben Van de Velde (Oct 25 2022 at 21:25):

This seems to compile, fwiw:

--- src/algebra/invertible.lean
+++ src/algebra/invertible.lean
@@ -5,7 +5,8 @@ Authors: Anne Baanen
 -/

 import algebra.group.units
-import algebra.ne_zero
+import algebra.group_with_zero.units
+--import algebra.ne_zero
 import algebra.ring.basic

 /-!
@@ -214,8 +215,8 @@ lemma nonzero_of_invertible [mul_zero_one_class α] (a : α) [nontrivial α] [in
 λ ha, zero_ne_one $ calc   0 = ⅟a * a : by simp [ha]
                          ... = 1 : inv_of_mul_self a

-@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
-  [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩
+--@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
+--  [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩

 section monoid_with_zero
 variable [monoid_with_zero α]

Eric Wieser (Oct 25 2022 at 23:46):

I think a nicer refactor would be to push ne_zero much lower

Eric Wieser (Oct 26 2022 at 00:07):

#17171

Mario Carneiro (Oct 26 2022 at 00:10):

what does leanproject import-graph give you after that PR @Eric Wieser ?

Scott Morrison (Oct 26 2022 at 02:10):

algebra.invertible.pdf

Scott Morrison (Oct 26 2022 at 02:14):

So it's a fair improvement (by avoiding data.nat.cast, we transitively avoid data.set.lattice and bunch of its imports).

Scott Morrison (Oct 26 2022 at 02:14):

But there's still a undigestible bolus of order theory coming in via data.nat.basic

Mario Carneiro (Oct 26 2022 at 02:31):

algebra.group_power.basic says:

The power operation on monoids and groups.
We separate this from group, because it depends on ``,
which in turn depends on other parts of algebra.

So it seems like this is expected for group power, but algebra.group_power.ring -> algebra.ne_zero now sounds even more suspicious

Mario Carneiro (Oct 26 2022 at 02:33):

yep, there is exactly one thing in the file that uses that bolus:

instance pow [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] : ne_zero (x ^ n) :=
pow_ne_zero n out

We can easily invert this dependency.

Scott Morrison (Oct 26 2022 at 03:08):

#17175

Scott Morrison (Oct 26 2022 at 03:20):

Hmmm, that still leaves us with algebra.ne_zero importing algebra.order.ring, because of

instance bit1 [canonically_ordered_comm_semiring M] [nontrivial M] : ne_zero (bit1 x) :=
mt (λ h, le_iff_exists_add'.2 _, h.symm⟩) zero_lt_one.not_le

I bet if we can move that as well we can really lower algebra.ne_zero and algebra.invertible.

Scott Morrison (Oct 26 2022 at 03:35):

#17176

Scott Morrison (Oct 26 2022 at 03:36):

Ah, nice. The supremum of #17171, #17174, #17175, and #17176 reduces the import hierarchy for algebra.invertible to:
algebra.invertible.sup.pdf, which is much more manageable.

Scott Morrison (Oct 26 2022 at 03:38):

I bet we could strip even more: surely logic.embedding is not really needed here. But not for now. :-)

Mario Carneiro (Oct 26 2022 at 03:51):

Well, I did :) #17177

Mario Carneiro (Oct 26 2022 at 03:58):

algebra.invertible.pdf

Mario Carneiro (Oct 26 2022 at 04:00):

now that dependency graph actually makes sense

Scott Morrison (Oct 26 2022 at 04:09):

#17179 will remove a further two nodes from that graph.

Scott Morrison (Oct 26 2022 at 04:14):

and #17180 another two. :-)

Ruben Van de Velde (Oct 26 2022 at 07:19):

Mario Carneiro said:

Well, I did :) #17177

Fwiw, you got a "rejected by label" from bors

Kevin Buzzard (Oct 26 2022 at 07:30):

What's the difference between light blue and dark blue again?

Yakov Pechersky (Oct 26 2022 at 07:39):

light blue is "all prereqs met", darker blue is "there is PR but it's not merged yet"

Yakov Pechersky (Oct 26 2022 at 07:41):

More precisely, "ready to start porting, all prereqs present" is turquoise1, "there is an unmerged PR" is lightskyblue

Kevin Buzzard (Oct 26 2022 at 08:02):

If I turn my data.bool.basic port branch into a PR (I got everything compiling yesterday for the first time, it's also a port of a core Lean file) then how does the system know there's a PR for data.bool.basic?

Yakov Pechersky (Oct 26 2022 at 08:03):

You have to edit the file here: https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

Kevin Buzzard (Oct 26 2022 at 08:03):

Got it -- sorry I'm learning a new trick here and it takes time

Jannis Limperg (Oct 26 2022 at 15:19):

(wrong thread again, why does this only happen to me?)

Scott Morrison (Nov 03 2022 at 03:01):

An update on porting progress. Here are some graphs for interesting targets:

Here's the list of currently available porting targets:

data.fun_like.basic
data.prod.basic    -- WIP
data.subtype
data.option.basic    -- PRd as mathlib4#493
logic.function.conjugate
data.nat.cast.defs
data.bool.basic    -- WIP Kevin Buzzard
logic.relation
control.functor
lean_core.data.vector
data.char
logic.lemmas
algebra.order.floor    -- Blocked by tactic.abel and tactic.linarith

(plus some lower priority stuff). It's tempting to believe that data.fun_like.[basic|embedding|equiv] could possibly be done as a single PR.

Scott Morrison (Nov 03 2022 at 03:02):

Both abel and linarith have open PRs that more-or-less work, so someone brave could start on algebra.order.floor by merging those branches into theirs.

Kevin Buzzard (Nov 05 2022 at 04:03):

I've taken a look at data.fun_like.basic and data.subtype and I think they're both beyond my pay grade. data.fun_like.basic assumes more about coercions than I know (but if someone wants to start me off I can have a go) and data.subtype uses stuff like initialize_simps_projections which I don't understand and might not even be ported yet.

Mario Carneiro (Nov 13 2022 at 02:13):

Could someone move the units section out of data.int.basic? That section requires more imports than everything else.

Moritz Doll (Nov 13 2022 at 03:38):

Mario are you on a recent branch? data.int.basic has two imports for me: data.nat.basic and order.monotone, the former is obviously necessary and the later is used only for

lemma coe_nat_strict_mono : strict_mono (coe :   ) := λ _ _, int.coe_nat_lt.2

Moritz Doll (Nov 13 2022 at 03:41):

and there is a file data.int.units already that imports algebra.group_power.order and lots of other stuff through data.int.order.basic

Scott Morrison (Nov 13 2022 at 04:13):

This change just landed in the last day or two.

Mario Carneiro (Nov 13 2022 at 04:18):

Note that I did not judge that by looking at the import line, but rather by the fact that the file is full of stuff that typechecks with almost no imports, and then there is a section at the bottom with a bunch of fancy things from mathlib algebra

Mario Carneiro (Nov 13 2022 at 04:19):

(I'm actually moving that file to Std so that section sticks out)

Scott Morrison (Nov 13 2022 at 05:10):

@Moritz Doll, are you still working on this?

Scott Morrison (Nov 13 2022 at 05:10):

(I'm tempted to have a look at rearranging to remove uses of units, but don't want to duplicate if you're already doing this.)

Moritz Doll (Nov 13 2022 at 05:11):

I don't really know how to do it properly, so it might be better if you do it

Scott Morrison (Nov 13 2022 at 05:32):

On it.

Scott Morrison (Nov 13 2022 at 05:53):

#17508

Michael Stoll (Nov 13 2022 at 09:51):

Scott Morrison said:

#17508

While you are doing that, can you perhaps include the additional lemmas from #17478 ?

Scott Morrison (Nov 13 2022 at 11:05):

Could you explain why that's better than two separate PRs?

Michael Stoll (Nov 13 2022 at 12:28):

Less work? If one gets merged, the other needs to be changed in any case, so why not do it right away? This probably saves some CI cycles, too.

Scott Morrison (Nov 13 2022 at 12:31):

Hmm... I'm conflicted. I like having the refactoring PRs neither add or remove material, so it's easier to be sure they are only refactors. :-)

Scott Morrison (Nov 13 2022 at 12:32):

But I do like not having things rot on the queue!

Michael Stoll (Nov 13 2022 at 12:48):

OK; I'll leave it to you to resolve this conflict :smile:.

Eric Wieser (Nov 13 2022 at 13:45):

I've sent #17478 to bors

Eric Wieser (Nov 13 2022 at 13:45):

Oh, I now see that the other one is also on the queue

Eric Wieser (Nov 13 2022 at 13:46):

I guess I'll let bors decide which one to spit out (or @Scott Morrison if you get there first)

Michael Stoll (Nov 13 2022 at 13:48):

They are in the same batch, so this batch will fail.

Eric Wieser (Nov 13 2022 at 14:05):

Bors will split the batch automatically if the merge conflicts

Michael Stoll (Nov 13 2022 at 16:12):

Looks like mine will get there first...

Eric Rodriguez (Nov 19 2022 at 17:44):

there's no real porting targets that seem open and mathematical right now, so what other tasks are there for someone wanting to get involved?

Eric Rodriguez (Nov 19 2022 at 17:45):

image.png for this section, is it about just eyeballing the files and making sure there's no big changes?

Heather Macbeth (Nov 19 2022 at 17:55):

After #17616 lands, I think it would be useful to do a similar task for data.list.big_operators. That file has a lot of imports. It lies on the path to data.list.perm and through that to data.fintype.basic, so anything you could strip from that path would be helpful.

Heather Macbeth (Nov 19 2022 at 17:57):

Or maybe we don't need big operators for the part of data.list.perm needed for fintype? So maybe the split should happen higher up? Anyway, I'm not sure, but it's worth looking into.

Heather Macbeth (Nov 19 2022 at 18:01):

It just doesn't seem like we should need lemmas about divisibility to define fintype ....

Jireh Loreaux (Nov 19 2022 at 18:11):

About the "the following files have been modified since the commit ...."

Two things:

  1. I think the plan is to at some point have a flag for the port_status script which will help you do this, but for now ...
  2. Take the file in question and git diff port-status-SHA master -- /path/to/file (in mathlib3). If the only change is the mathlib4 synchronization label, then update the port-status page for the file with the current SHA from mathlib master.

If there are new changes to the file, then port the new changes to mathlib4 (or make sure they are already there somehow).

Patrick Massot (Nov 19 2022 at 18:14):

Eric Rodriguez said:

there's no real porting targets that seem open and mathematical right now, so what other tasks are there for someone wanting to get involved?

Porting targets that are not mathematical.

Jireh Loreaux (Nov 19 2022 at 18:26):

To second Patrick's point, you are likely capable of porting the non-mathematical things, e.g., I doubt data.stream.defs would be that hard, but I haven't looked carefully.

Arien Malec (Nov 19 2022 at 19:56):

I’ve been following a heuristic of “not deeply mathematical” and ideally non-critical path & if I can do some grunt work that helps more experienced folks hone in on the hard bits that’s fine too. Helps to have a generally high tolerance for grunt work or wasted effort if it helps expose issues (see my many adventures discovering things already in Std or only on critical path for tactics)

Eric Rodriguez (Nov 19 2022 at 20:25):

I felt less confident about them because I'm more likely to mess up important meta-details; I'll still give it a shot, though

Arien Malec (Nov 19 2022 at 20:29):

I prefer to change little, not make any change that I don’t understand, and comment on any uncertainty….

Eric Rodriguez (Nov 19 2022 at 20:43):

Jireh Loreaux said:

About the "the following files have been modified since the commit ...."

Two things:

  1. I think the plan is to at some point have a flag for the port_status script which will help you do this, but for now ...
  2. Take the file in question and git diff port-status-SHA master -- /path/to/file (in mathlib3). If the only change is the mathlib4 synchronization label, then update the port-status page for the file with the current SHA from mathlib master.

If there are new changes to the file, then port the new changes to mathlib4 (or make sure they are already there somehow).

I've just made #17630, which adds a simple option that outputs the required git diff command. Hopefully it makes it less work to check this.

Eric Rodriguez (Nov 19 2022 at 20:55):

using this script patch, I very coarsely verified that the following files are ported okay (I excluded any files that had even a non-trivial import change for quick checking):

If anyone else can verify these, I'll change these's SHAs on the status page

Eric Rodriguez (Nov 19 2022 at 20:55):

(a helpful git option was git config pager.diff false

Jireh Loreaux (Nov 19 2022 at 20:57):

Note: your script should diff against master, not HEAD

Jireh Loreaux (Nov 19 2022 at 20:57):

Just in case someone is on another branch without realizing it.

Eric Rodriguez (Nov 19 2022 at 21:00):

Do you think I should make that change generally to the script or just when outputting? I wonder if this current functionality is useful for someone preparing a PR to do with mathlib4

Eric Rodriguez (Nov 19 2022 at 21:14):

Jireh Loreaux said:

To second Patrick's point, you are likely capable of porting the non-mathematical things, e.g., I doubt data.stream.defs would be that hard, but I haven't looked carefully.

oh, there's another definition of Stream already

Jireh Loreaux (Nov 19 2022 at 22:09):

I ran all the diffs against c4658a649d216f57e99621708b09dcb3dcccbd23 on master. Looks like data.bool.basic can also go on your list. However, I think the following fileshave changes (and I have not checked them against mathlib4). If you checked them against mathlib4, that's fine, but if you haven't don't update the SHAs.

  • order.compare
  • category_theory.concrete_category.bundled
  • logic.equiv.defs
  • data.subtype
  • data.fun_like.equiv

Jireh Loreaux (Nov 19 2022 at 22:12):

If you have time and are willing, you could synchronize the files that need it with mathlib4, but I don't have time tonight to try and do that.

Eric Rodriguez (Nov 19 2022 at 22:14):

Okay, I checked most of those manually as well (just proof changes apart from fun_like.equiv). I'll put these in and maybe I'll fix discrepancies on others later

Scott Morrison (Nov 19 2022 at 23:41):

Looking at the state of things this morning, the really really helpful thing that people can do is review each others PRs (e.g. check #align's, fix errors, mark as approved), and then post in a thread here requests for merging (or merge yourself if you self-identify as someone who should do that :-)

Scott Morrison (Nov 19 2022 at 23:41):

We have a big PR queue.

Scott Morrison (Nov 19 2022 at 23:41):

If someone could add the #queue4 linkifier that would be lovely.

Scott Morrison (Nov 19 2022 at 23:42):

Oh! It exists. :-)

Scott Morrison (Nov 19 2022 at 23:42):

Okay --- go forth and review all those PRs, and anything that looks ready to go, hunt down someone who will hit bors merge on it. :-)

Scott Morrison (Nov 19 2022 at 23:42):

I am soon to be essentially offline for 72 hours, due to some complicated travel.

Scott Morrison (Nov 19 2022 at 23:52):

Priorities for attention should be #641 and #631.

Eric Rodriguez (Nov 19 2022 at 23:53):

mathlib4#641, mathlib4#631

Eric Rodriguez (Nov 19 2022 at 23:53):

Is there any chance we could ask people to in future just commit the raw mathbin file as the first commit?

Scott Morrison (Nov 19 2022 at 23:54):

Yes! It's been suggested before. @Eric Rodriguez, would you verify that it is in the wiki?

Eric Rodriguez (Nov 19 2022 at 23:54):

No, it hasn't. I'll add it now

Scott Morrison (Nov 20 2022 at 00:00):

In fact, I'd say mathlib4#641 is ready to go, except for the library_note "coercion into rings" needing updating.

Scott Morrison (Nov 20 2022 at 00:01):

If @Gabriel Ebner would be willing to either rewrite that, or just say "please leave a 'Porting note' that this library note is out of date and needs repair", then I think we should merge.

Gabriel Ebner (Nov 20 2022 at 00:07):

Okay I've rewrote the library note.

Scott Morrison (Nov 20 2022 at 00:08):

Haha, great, the solution was to delete the confusing paragraph. :-)

Arien Malec (Nov 20 2022 at 00:38):

I believe mathlib4#616 and mathlib4#649 are good to go pending review. mathlib4#638 has a universe linting error if good just needs an override.

Jireh Loreaux (Nov 20 2022 at 01:50):

Probably you should fix the universe linting error. Let me know if you need help.

Arien Malec (Nov 20 2022 at 02:07):

I definitely need help -- not sure what's causing it...

Jireh Loreaux (Nov 20 2022 at 02:33):

I'll try to have a quick look in an hour or so.

Arien Malec (Nov 20 2022 at 02:47):

The reason I think this is OK is that it occurs in the typeclass instances for ULift which is designed to do universe shenanigans. In particular, the lint is for "max u v in the type where neither u nor v occur by themselves" but ULift by definition maps to Type (max s r)

Mario Carneiro (Nov 20 2022 at 02:50):

The lint is for when u and v appear together as max u v everywhere in the declaration and proof. If you use ULift.{u, v} then u and v are appearing separately

Arien Malec (Nov 20 2022 at 02:54):

The code is never using max u v; this only happens behind the scenes in the typeclass instance. It's possible I need a fix by adding explicit universe types for all the invocations of ULift?

Mario Carneiro (Nov 20 2022 at 03:05):

I mean the elaborated term uses max u v

Mario Carneiro (Nov 20 2022 at 03:06):

(If you have a specific example in mind you should probably do it on another thread, this one is about porting requests and progress toward them)

Casavaca (Jan 03 2023 at 05:50):

I just picked up a light blue node and ported it. Is this change desired? https://github.com/leanprover-community/mathlib4/pull/1307 Port/order.concept

Casavaca (Jan 05 2023 at 16:19):

Anyone interested to help me with this pull request?

Kevin Buzzard (Jan 05 2023 at 17:02):

Usually pull requests are made from branches of leanprover-community/mathlib4 ; I'm not sure your PR will ever make it onto #queue4 because it hasn't been done in this way. Why not ping the maintainers letting them now your github userid and ask for push access to non-master branches of mathlib4? I don't ever look at the PRs in mathlib4, I only ever look at #queue4 because those are the PRs which are "ready for review".

Casavaca (Jan 05 2023 at 17:38):

That's helpful. Thanks.

Kevin Buzzard (Jan 05 2023 at 22:26):

PS I also looked at your PR today given that you flagged it explicitly :-)


Last updated: Dec 20 2023 at 11:08 UTC