search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

Move polynomial section, fix df-mhp, + mhpvarcl #4014

Closed icecream17 closed 2 months ago

icecream17 commented 3 months ago

and + fsuppind (mathbox)

Fixes #3995

wlammen commented 3 months ago

14,250 additions, 14,087 deletions not shown because the diff is too large. Please use a local Git client to view these changes.

This is what I get when I want to look at the diff in my browser. Does it mean I have to download the fork icecream17:move onto my computer to see there what you are requesting? Can't the move be broken up in pieces small enough to allow usual reviews?

icecream17 commented 3 months ago

I split the first commit into two parts. As seen by the checks, the resulting code is the same

This should be within the diff limits by github: https://docs.github.com/en/repositories/creating-and-managing-repositories/repository-limits#diff-limits

icecream17 commented 3 months ago

Can still review, but draft pending conversation at #3995

tirix commented 3 months ago

This moves big chapters around, so the chances of conflicts are high (e.g. if we add theorems from mathboxes to the moved sections). Maybe we should not wait for too long with this?

icecream17 commented 2 months ago

Perhaps it would be helpful to split this pr into two, and have one pr move the sections, while the other fixes df-mhp?

A follow up pr would be necessary anyway since the Associative Algebra section would be moved too (as suggested by @benjub), and I would have to make a version of fsuppind for homogeneous polynomials.

wlammen commented 2 months ago

While it is certainly a good idea to do just one thing per pull request, I think it does not help here a lot. To me, it seems people are awaiting @digama0 's confirmation (https://github.com/metamath/set.mm/issues/3995#issuecomment-2132270652). The last post of him here on github I remember, is this one https://github.com/metamath/set.mm/issues/3990#issuecomment-2124160362 . So either he is awfully busy, or on vacation, or... Is his approval imperative, so we cannot proceed without it? If possible, we should allow (slow?) development, even if he is known to be an expert in this field. I don't like the idea, that otherwise contributions get blocked for an unknown, at least long time, before a decision is made. This holds the more when the pull request is easily revertible.

icecream17 commented 2 months ago

I propose to just merge for now, per tirix and wlammen, then.

The one week time period has elapsed but it's a gray area since I don't have write access/merge permissions

wlammen commented 2 months ago

I've seen no objection to this pull request, other than "Lets wait and see what others say". On the other side there is confirmation by @tirix and @benjub for it. If this state does not change until weekend, I will merge it.