Freeze of mathlib3

Stream: general

[Yury G. Kudryashov]

Creating a thread for questions about the freeze of mathlib3.

[Yury G. Kudryashov]

Yury G. Kudryashov said:

Dear mathlib users,

As more than 90% of mathlib is already ported to Lean 4, we (the maintainers) made the following decisions about freezing mathlib 3.

• We encourage the authors to move the development to mathlib4 as soon as relevant parts of the library is ported. While we are not going to accept "refactors" for now, new features are accepted. You may want to use oneshot mathport to port your existing lean 3 file to lean 4.
• Mathlib 3 PRs that have been marked awaiting-review and have a greenlight from the CI by the end of July 14 AOE 2023-07-15T00:00:00-12:00 will be considered individually, and we will decide if it shall go through the same "review; merge; forward-port" process that we use now. Meeting the deadline is a necessary but not a sufficient condition to have your PR merged into mathlib 3. E.g., if you're adding a new file, then we will probably ask you to port it yourself and PR to mathlib 4 so that we review it once instead of twice.
• All other mathlib 3 PRs will be marked with a new label too-late and will not be reviewed. We will not close them because authors may use them, e.g., as a reminders to forward-port them and reopen in mathlib4 repo.
• We still intend to support everyone who is moving code from Lean 3 to Lean 4, and can provide advice on using mathport on individual files and separate projects. This announcement is not the end of that process: simply the end of merging new content to mathlib3.

Yours,
Maintainers team

[Pedro Sánchez Terraf]

I have !3#17972 on the waiting list. I didn't have time to prepare the ported version, but when I finally tried to use mathport it seemed as one of my imports did not exist in mathlib4, at least not with corresponding capitalized name (the original one is here).

I need this for induction'. Where is this located? Thanks in advance!

[Kevin Buzzard]

import Mathlib.Tactic will give you induction' and then you can just right click on it to find where it actually is.

[Calvin Lee]

!3#17973 is on the waiting list, and I'd rather just move it to mathlib4.
However, this PR uses some clever conv tricks. In particular, it uses for patterns in conv that seem to work differently than with pattern.
In lean3, for will return to the top level expression after executing a conv mode command on each matched expression. However, pattern seems to leave conv in a subexpression after the matches are executed.

Is there any good documentation on lean4 conv mode, or docs on how to move from lean3 to lean4 conv? Most examples that I found in mathlib just abandoned pattern, or only use it once.

[Kevin Buzzard]

FWIW I reviewed !3#17973 . I think the conv questions you raise here are great.

[Calvin Lee]

since I'm planning on closing this PR in favor of a mathlib4 one, I'll be responding to these comments on !4#5766

[Kyle Miller]

Calvin Lee said:

In lean3, for will return to the top level expression after executing a conv mode command on each matched expression.

Is this what you're looking for? You can use a sub-conv to temporarily focus on a goal, navigate (using pattern for example), do transformations, and then after the sub-conv you have the transformed version of the goal.

conv =>
  ...
  conv =>
    pattern t
    -- do transformations
    ...
  -- now we're back but with a transformed goal
  ...

(Linking to your other thread for anyone who might come across this message, here's a rough guide to everything you can do with Lean 4 conv mode: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/conv.20documentation/near/373668019)

[Calvin Lee]

indeed
this is the commit that fixed everything https://github.com/leanprover-community/mathlib4/pull/5766/commits/6d8d90501764606634fb73514e67049562048ea3

[Mauricio Collares]

This was probably not intentional, but here's a fun fact: The mathlib 3 cutoff date is 15th July 2023 (almost everywhere I guess), which is exactly 10 years after Leo's first Lean commit on Mon Jul 15 18:43:32 2013 -0700.

[Henrik Böving]

coincidence?!?!!!

[Scott Morrison]

Pedro Sánchez Terraf said:

I have !3#17972 on the waiting list. I didn't have time to prepare the ported version, but when I finally tried to use mathport it seemed as one of my imports did not exist in mathlib4, at least not with corresponding capitalized name (the original one is here).

I need this for induction'. Where is this located? Thanks in advance!

@Pedro Sánchez Terraf, what is the status here? Should we try to review the mathlib3 PR, or can that be closed and you'll open a new Mathlib4 PR to replace it?

[Pedro Sánchez Terraf]

I think it is better to close it, since it sightly modifies other files.
Thanks for asking.

PST.-

—sent from mobile

El mar, 25 de jul de 2023, 02:33, Zulip notifications <noreply@zulip.com>
escribió:

[Scott Morrison]

Thanks, I've closed it.