Zulip Chat Archive

Stream: mathlib4

Topic: algebra.module.localized_module

Ruben Van de Velde (May 14 2023 at 19:23):

algebra.module.localized_module has a porting note asking to wait for #17973, which hasn't been touched this year. Can we either move that forward or not block on it?

Eric Wieser (May 14 2023 at 21:05):

(note that primary intent of these porting notes is to ensure the Zulip discussion happens, not necessarily to block the port)

Eric Wieser (May 14 2023 at 21:06):

@Calvin Lee, do you think you'll have time to come back to this?

Calvin Lee (May 14 2023 at 21:07):

Yep! Happy to help port it

Eric Wieser (May 14 2023 at 21:08):

The choice here is:

  1. Finish off the mathlib3 PR, get it merged, then port it
  2. Port it immediately, and forward-port the mathlib3 PR if it gets merged

Eric Wieser (May 14 2023 at 21:09):

This looks pretty easy to forward-port, so I think I agree with Ruben that option 2 is fine

Eric Wieser (May 14 2023 at 21:09):

(if you had majorly refactored the file then option 1 would be a better choice)

Ruben Van de Velde (May 14 2023 at 21:32):

I didn't really mean to express a preference, but (2) certainly feels easiest from the perspective of someone who's mostly been porting recently :)

Calvin Lee (May 15 2023 at 01:37):

yep! option 2 sounds fine. I just wanted to have a discussion about this :)

Calvin Lee (May 15 2023 at 01:40):

I also went and removed the porting note, since we've decided against waiting.

Yuma Mizuno (May 15 2023 at 13:08):

Sorry, I was working on porting !4#3993 without noticing the thread. I'm almost done, but I'm stuck at Semiring (LocalizedModule S A) timeout. Any help would be appreciated.

Yuma Mizuno (May 16 2023 at 22:06):

Porting of the original file completed !4#3993. @Calvin Lee Could you port PR #17973 now?

Calvin Lee (May 16 2023 at 22:06):

Yes, I am just waiting for the original PR to be merged, as we agreed upon in this thread.

Last updated: Dec 20 2023 at 11:08 UTC