Zulip Chat Archive

Stream: mathlib4

Topic: !4#3654 IsROrC

Scott Morrison (Apr 28 2023 at 02:26):

@Yury G. Kudryashov, it looks like you may have forgotten to commit the file Mathlib/Data/IsROrC/Attr.lean?

Yury G. Kudryashov (Apr 28 2023 at 04:20):

Indeed, thanks!

Yury G. Kudryashov (Apr 28 2023 at 04:21):

Why did you merge master?

Scott Morrison (Apr 28 2023 at 05:53):

Hmm, maybe I shouldn't do this --- I change branches very frequently, and if the Lean 4 version has changed across branches I find I have a harder time syncing the oleans. Hence when I come across a branch with an apparently old Lean 4 version (evidenced by a pop-up in VSCode), I tend to merge master to avoid this.

Yury G. Kudryashov (Apr 28 2023 at 21:28):

The PR was not help-wanted at the moment. I had to merge remote to push Attr.lean, thus postpone my work on this branch while waiting for CI.

Scott Morrison (Apr 28 2023 at 23:27):

I'm sorry. :-(

Jeremy Tan (Apr 29 2023 at 12:12):

There are two linter FAILURES left in this file; how do we work around them?

Jeremy Tan (Apr 29 2023 at 12:15):

Is it the same old trick of specifying the simp lemmas to generate?

Eric Wieser (Apr 29 2023 at 12:17):

Jeremy, note that Yury probably doesn't want help here yet as they are trying to refactor mathlib3 at the same time

Jeremy Tan (Apr 29 2023 at 12:17):

But where is that refactor?

Yaël Dillies (Apr 29 2023 at 12:19):

From the PR description: "I'm going to backport them". So the PR hasn't been opened yet.

Yury G. Kudryashov (May 02 2023 at 20:12):

I failed to open it before I had to switch to some other tasks. Here it is: #18919

Eric Wieser (May 02 2023 at 20:25):

Ouch, that's an awfully large number of refactors at once

Yaël Dillies (May 02 2023 at 21:56):

I will try to review it this friday

Eric Wieser (May 02 2023 at 22:27):

I found an easy split to reduce the number of touched files, #18922

Eric Wieser (May 02 2023 at 22:54):

(I should perhaps add to my negative comment above that Yury G. Kudryashov's PR is full of great golfs and cleanups, and losing 300 lines overall is great!)

Yury G. Kudryashov (May 03 2023 at 02:50):

I'm sorry for combining many refactors in one PR. I'll try to cherry-pick smaller PRs from it.

Yury G. Kudryashov (May 03 2023 at 06:07):

I moved some parts to #18927, #18928

Eric Wieser (May 07 2023 at 21:51):

Thanks for all the splits! I've delegated #18919, which I assume is the final piece; it now looks pretty uncontroversial, and removes a significant number of lines. I haven't checked too carefully that we didn't drop any lemmas by accident, but they're all trivial results anyway so it's not a big deal if so.

Yury G. Kudryashov (May 08 2023 at 21:44):

Thanks for the review! Merged, waiting for mathport.

Last updated: Dec 20 2023 at 11:08 UTC