Zulip Chat Archive

Stream: PR reviews

Topic: older ports

Ruben Van de Velde (Apr 08 2023 at 06:14):

I spent some time resurrecting some old port PRs, would be nice to get a review on them:

Scott Morrison (Apr 08 2023 at 12:19):

I think we probably shouldn't be porting Data.Array.Lemmas at all. Is it used anywhere downstream? Arrays are all new and better in Lean 4.

Jeremy Tan (Apr 08 2023 at 12:21):

parclytaxel@parclytaxel-winterthur:~/Documents/Computing/Repos/mathlib3port$ git grep "import Mathbin.Data.Array"
Mathbin/All.lean:import Mathbin.Data.Array.Lemmas
Mathbin/Data/Buffer/Basic.lean:import Mathbin.Data.Array.Lemmas
Mathbin/Data/HashMap.lean:import Mathbin.Data.Array.Lemmas

Jeremy Tan (Apr 08 2023 at 12:22):

so the file is used downstream

Jeremy Tan (Apr 08 2023 at 12:26):

in turn mathlib3's polyrith tactic depends on Data.Buffer.Basic

Ruben Van de Velde (Apr 08 2023 at 13:09):

Yeah, it's used in a few places that arguably shouldn't be ported either, like Logic.Equiv.Array as well. polyrith already has been ported without it. We should mark them unportable in the wiki if that's the decision, though

Scott Morrison (Apr 08 2023 at 21:50):

@Ruben Van de Velde, would you mind marking as unportable? (Also for Data.HashMap and Data.Buffer.Basic)

Scott Morrison (Apr 09 2023 at 07:26):

I've marked these as not needed at https://github.com/leanprover-community/mathlib4/wiki/port-comments

Ruben Van de Velde (Apr 10 2023 at 10:37):

Ruben Van de Velde said:

I spent some time resurrecting some old port PRs, would be nice to get a review on them:

Data.Finset.Sups is done, Data.Array.Lemmas is dropped, Order.Height just needs a maintainer to put it on the queue and the others are up for review.

Scott Morrison (Apr 10 2023 at 11:19):

Just hit merge on Order.Height.

Jeremy Tan (Apr 10 2023 at 12:33):

!4#3248 needs review too

Jeremy Tan (Apr 10 2023 at 12:34):

!4#3362, which fully forwardports three separate files, is ready for review too

Ruben Van de Velde (Apr 10 2023 at 12:35):

I don't think either of those counts as old PRs :)

Jeremy Tan (Apr 10 2023 at 12:36):

Well we need to get the queue down to 20

Jeremy Tan (Apr 10 2023 at 12:37):

!4#3248 has the highest import depth

Eric Wieser (Apr 10 2023 at 12:38):

Jeremy Tan said:

Well we need to get the queue down to 20

We don't urgently need to do that, it's just a target for people who want to continue modifying mathlib3

Ruben Van de Velde (Apr 11 2023 at 08:27):

The following are also ready for review:

Ruben Van de Velde (Apr 14 2023 at 13:36):

Next up:

  • RingTheory.NonUnitalSubsemiring.Basic !4#1774
  • NumberTheory.LucasLehmer !4#2988

Ruben Van de Velde (Apr 14 2023 at 14:30):

And

  • Analysis.BoxIntegral.Box.Basic !4#2625

Jeremy Tan (Apr 26 2023 at 06:18):

(deleted)

Jeremy Tan (Apr 26 2023 at 12:22):

!4#3656 is ready BTW

Jeremy Tan (Apr 26 2023 at 15:07):

@Eric Wieser :up:

Ruben Van de Velde (May 15 2023 at 08:25):

Data.Polynomial.Laurent !4#2953 is up for review

Last updated: Dec 20 2023 at 11:08 UTC