Zulip Chat Archive

Stream: mathlib4

Topic: modified since verified

Johan Commelin (Dec 02 2022 at 06:51):

What should we do with this list

    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/group/commute.lean
    git diff 71ca477041bcd6d7c745fe555dc49735c12944b7..HEAD src/algebra/order/sub/defs.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/algebra/order/monoid/order_dual.lean
    git diff 99e8971dc62f1f7ecf693d75e75fbbabd55849de..HEAD src/algebra/order/monoid/lemmas.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/order/monoid/defs.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/order/monoid/min_max.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/algebra/order/monoid/cancel/defs.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/algebra/order/monoid/canonical/defs.lean
    git diff 99e8971dc62f1f7ecf693d75e75fbbabd55849de..HEAD src/algebra/order/hom/basic.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/group_with_zero/semiconj.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/group_with_zero/commute.lean
    git diff 71ca477041bcd6d7c745fe555dc49735c12944b7..HEAD src/algebra/group_with_zero/units/basic.lean
    git diff 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3..HEAD src/algebra/field/defs.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/hom/embedding.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/ring/semiconj.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/algebra/ring/commute.lean
    git diff 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..HEAD src/algebra/ring/regular.lean
    git diff a148d797a1094ab554ad4183a4ad6f130358ef64..HEAD src/logic/embedding/basic.lean
    git diff 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3..HEAD src/logic/equiv/option.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/order/bounded_order.lean
    git diff 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..HEAD src/order/prop_instances.lean
    git diff a148d797a1094ab554ad4183a4ad6f130358ef64..HEAD src/order/basic.lean
    git diff 71ca477041bcd6d7c745fe555dc49735c12944b7..HEAD src/order/min_max.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/order/disjoint.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/order/with_bot.lean
    git diff 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..HEAD src/control/applicative.lean
    git diff a148d797a1094ab554ad4183a4ad6f130358ef64..HEAD src/control/functor.lean
    git diff 76171581280d5b5d1e2d1f4f37e5420357bdc636..HEAD src/control/monad/basic.lean
    git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/data/int/units.lean
    git diff d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..HEAD src/data/int/cast/basic.lean
    git diff 7ac96dea0572f31067e9e35bebbecef7fa3fa91a..HEAD src/data/nat/basic.lean
    git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/data/nat/psub.lean
    git diff 62a5626868683c104774de8d85b9855234ac807c..HEAD src/data/nat/units.lean
    git diff a148d797a1094ab554ad4183a4ad6f130358ef64..HEAD src/data/pi/algebra.lean
    git diff 71ca477041bcd6d7c745fe555dc49735c12944b7..HEAD src/data/countable/defs.lean
    git diff 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a..HEAD src/data/prod/lex.lean

Johan Commelin (Dec 02 2022 at 06:51):

90% of the diffs are

+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/736
+> Any changes to this file require a corresponding PR to mathlib4.
+

Johan Commelin (Dec 02 2022 at 06:51):

Should we now update some hashes somewhere?

Yury G. Kudryashov (Dec 02 2022 at 06:59):

You can update hashes here: https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

Johan Commelin (Dec 02 2022 at 07:15):

Hmm, I guess we should try to automate that. Because editing that huge wiki by hand sounds like a disaster waiting to happen.

Jireh Loreaux (Dec 02 2022 at 07:19):

I'm fine if someone automates this, but I've done this and it's not so bad.

Riccardo Brasca (Dec 02 2022 at 08:35):

Note that you can just the last hash for every file if the difference is those 4 lines, so the same hash for everything

Riccardo Brasca (Dec 02 2022 at 08:35):

In any case I am going to do ti by hand after the coffee

Jakob von Raumer (Dec 02 2022 at 08:40):

Huh, started doing it simultaneously with you, I'll stop then :sweat_smile:

Riccardo Brasca (Dec 02 2022 at 08:42):

You can start from the bottom if you want :D

Jakob von Raumer (Dec 02 2022 at 08:42):

Yes, let's meed in the middle :D

Riccardo Brasca (Dec 02 2022 at 08:43):

I will stop at src/algebra/order/monoid/min_max.lean

Jakob von Raumer (Dec 02 2022 at 08:43):

Johan Commelin said:

Hmm, I guess we should try to automate that. Because editing that huge wiki by hand sounds like a disaster waiting to happen.

I think we wouldn't even have to look at the diff. We just need to make sure that the CI commit that adds the comment is the only one that's touched the file since the hash

Riccardo Brasca (Dec 02 2022 at 08:43):

Just save the file every time

Jakob von Raumer (Dec 02 2022 at 09:00):

What's the idea about the edited ones? Just re-port them or report them to the one who edited them and tell them it's their obligation to port

Riccardo Brasca (Dec 02 2022 at 09:02):

What I am doing is having a quick look to see if I can take responsibility to update the hash. If I don't know my plan is to ping the authors of edit

Eric Wieser (Dec 02 2022 at 09:19):

We should update the script to exclude such diffs automatically

Eric Wieser (Dec 02 2022 at 09:20):

That is:

Create a temporary copy of the original mathlib file with the comment removed
Create a temporary copy of the master mathlib file with the comment removed
Compute the diff

Riccardo Brasca (Dec 02 2022 at 09:23):

Yes, I agree we should have a script for this.

Eric Wieser (Dec 02 2022 at 09:23):

My claim is we should not update the SHAs at all

Eric Wieser (Dec 02 2022 at 09:23):

They should only be updated if someone actually synchronized the content

Riccardo Brasca (Dec 02 2022 at 09:24):

Ah, that's a possibility

Eric Wieser (Dec 02 2022 at 09:24):

I think git's --ignore-matching-lines may work in our favor here

Eric Wieser (Dec 02 2022 at 09:24):

I'll have a quick go at updating the script

Riccardo Brasca (Dec 02 2022 at 09:25):

In any case it is now updated, so I am pinging
@Heather Macbeth about #17758
@Yaël Dillies about #16761 and #17734
Can you check if the modifications you made to mathlib3 also exist in mathlib4? Thanks!

Eric Wieser (Dec 02 2022 at 09:31):

I can't test the script if it's updated :(

Riccardo Brasca (Dec 02 2022 at 09:32):

Oh, sorry! You can just revert my last modification to a file to test

Heather Macbeth (Dec 02 2022 at 09:37):

@Riccardo Brasca Regarding #17758, see my comment on the PR:

This PR touches a frozen file (algebra/order/hom/basic) but only for meta code, which I believe is permissible.

Eric Wieser (Dec 02 2022 at 09:45):

#17788

Eric Wieser (Dec 02 2022 at 09:46):

Would also be good to get #17756 in so that the bot that adds these comments comes back from the dead

Yaël Dillies (Dec 02 2022 at 10:38):

mathlib4#768 took care of #17734. I totally forgot about #16761 so I'll do it now.

Riccardo Brasca (Dec 02 2022 at 10:43):

No worries!

Riccardo Brasca (Dec 02 2022 at 10:48):

@Eric Wieser your script will take care of

The following files are marked as ported, but do not have a SYNCHRONIZED WITH MATHLIB4 label.
...

automatically, right?

Eric Wieser (Dec 02 2022 at 10:50):

Yes, #17756 will do that. The script is in master and was working in the past, but was broken by some header comments in a format I didn't expect. #17756 fixes that particular bug in the script.

Riccardo Brasca (Dec 02 2022 at 10:51):

Nice! I prefer not to merge it since I don't know python, but I am confident someone will do it quickly

Eric Wieser (Dec 02 2022 at 10:53):

#17790 is an example of a PR generated by that PR. Right now I have to run it manually because the cron job runs the broken version on master (edit: and it produces an inaccurate list of changes because it's comparing to my branch not master!)

Riccardo Brasca (Dec 02 2022 at 10:58):

#17790 looks good to me. What's wrong with it?

Riccardo Brasca (Dec 02 2022 at 10:58):

Ah, the message

Riccardo Brasca (Dec 02 2022 at 11:08):

I've fixed it by hand.

Eric Wieser (Dec 02 2022 at 11:09):

I think better to leave it to test the bot

Riccardo Brasca (Dec 02 2022 at 11:13):

Ah, I messed up the message trying to go back to the original version, I am sorry

Eric Wieser (Dec 02 2022 at 11:20):

Don't worry, the bot will overwrite it

Jakob von Raumer (Dec 02 2022 at 11:28):

Should CI give a warning about changing frozen files without a linked mathlib4 PR?

Eric Wieser (Dec 02 2022 at 11:33):

Yes, definitely; that was the next bot on my TODO list

Eric Wieser (Dec 02 2022 at 11:34):

(strictly the warning should be triggered by changing files mentioned on #port-wiki, not by the presense of a freeze comment)

Eric Wieser (Dec 02 2022 at 11:34):

Probably it should just be an error rather than a warning, as that avoids race conditions if mathlib changes while things are in the bors queue

Last updated: Dec 20 2023 at 11:08 UTC