triage of "Porting notes"

Stream: mathlib4

[Scott Morrison]

As discussion in today's porting meeting, we now have around 7500 porting notes scattered through mathlib4. This represents some significant technical debt that we are going to have to gradually pay down.

Some aspirational proposals, which perhaps we should have talked about earlier. :-)

1. Please put porting notes immediately before the code you're discussing, not on the line after.
2. When making a porting note about a broken proof, please try to provide complete context in the porting note. In particular, please leave the original mathport output in a comment with the porting note, so that it is not necessary for someone diagnosing the porting note to open either the mathlib3port repository or the mathlib repository to even understand what has changed.
3. We'd like to be able to classify porting notes, e.g. to be able to find all porting notes which are discussing a simp regression. The proposal from today's meeting is that we belatedly start using more issues, on the mathlib4 repository, and aspirationally porting notes can either be resolved immediately, or have a link to some issue included. These issues can be open-ended, like "simp isn't doing what I expected", or more focused, but something is better than nothing.

[Scott Morrison]

As an example of this last point, I just created https://github.com/leanprover-community/mathlib4/issues/4998, which describes a slight change in behaviour of anonymous constructor syntax between lean3 and lean4 (you can't use auto_params). It's not intended to be a bug report: the change here is really just that auto_params are no longer a separate thing from default values, and anonymous constructor notation never relied on default values in lean3 or lean4.

Nevertheless, it's something we can link to if we're writing a porting note about having to fill in an extra argument like this. As an example, I just linked to this issue here: https://github.com/leanprover-community/mathlib4/pull/4984/files#diff-b86b96716b4a0fb8c2e711030691f4b727c0f615eceaf05a1ac75083873e444dR46.

[Scott Morrison]

I appreciate that this is pretty "aspirational", but we do have to face that this backlog of porting notes is going to be weighing on us for a while to come, and we need to get a bit more organised about how we're going to deal with them.

[Scott Morrison]

So please don't feel like this is an additional burden which is going to get in the way of finishing the port. It's just intended as an idea about how we can best approach all the work that comes after the port is "100% done". :-)

[Eric Wieser]

Can we establish a standard format for referring to a mathlib4 issue from a porting note? Perhaps

-- Porting note (mathlib4#4998): the message

which has the advantage that we can more easily measure how many notes are issue-less

[Scott Morrison]

Yes, I wanted to do that, but was stumped by the lack of linkifiers in VSCode, without which this is worse than a URL.

[Scott Morrison]

Oh, didn't we do this with library notes in mathlib3?

[Scott Morrison]

I guess that is actually in the VSCode extension??

[Eric Wieser]

I would guess there is a GitHub vscode extension that can handle this without it needing to be part of the lean extension

[Mario Carneiro]

github doesn't recognize mathlib4#4998 for linkification, you would need to spell it leanprover-community/mathlib4#4998

[Scott Morrison]

I think full URLs will be best for now. :-)

[Ruben Van de Velde]

Should we have a list of changes that don't need porting notes? Removing include/omit, for example

[Scott Morrison]

Sounds good. An non-exhaustive list of things that don't need porting notes:

• removing omit/include
• removing -- mathport name:
• removing restate_axiom (as long as you remove the ' on the field name
• replacing @[protect_proj] with protected fields (perhaps this is automatic now?)

along with more obvious ones:

• following linter instructions (renaming unused arguments to _, replacing unnecessary <;> with ;, removing unused haves)

[Eric Wieser]

Does replacing apply foo.induction_on x with induction x using foo.induction_on with need a note?

[Eric Wieser]

Often the former fails to elaborate, but the latter is a nicer spelling anyway (but didn't work in mathlib3)

[Scott Morrison]

I'd say no!

[Mario Carneiro]

Scott Morrison said:

• removing omit/include
• removing -- mathport name:

you know, you can always just request for mathport to stop adding things if you are just consistently deleting them without comment

[Jireh Loreaux]

I think here we are more concerned that we are deleting them with comment. :laughing:

[Mario Carneiro]

right, but my point is that this is unnecessary work and people aren't reporting mathport issues enough

[Eric Wieser]

While we're there, I think we should nuke the #print correctly_ported /-- old code -/ behavior

[Eric Wieser]

It's pretty useless since the vast majority of declarations are not "correctly ported", and it gets in the way of forward-porting

[Jireh Loreaux]

How impossible is it to try to align instances from the bottom up? It would be nice to know how may "actually" dubious translations we have, as opposed to ones which only differ because of unaligned instances.

[Eric Wieser]

I think that would be really value if just for cross-linking between the docs

[Jireh Loreaux]

We also need a fix for the instance name generator. Is there an issue for this already?

[Mario Carneiro]

Eric Wieser said:

While we're there, I think we should nuke the #print correctly_ported /-- old code -/ behavior

What do you want it to show instead? old code?

[Eric Wieser]

Yes, because it already does that for like 2/3 of fully-ported files anyway

[Mario Carneiro]

2/3?

[Mario Carneiro]

I would have expected a proportion closer to 10-20%

[Mario Carneiro]

I guess I don't really understand what you mean by "the vast majority of declarations are not 'correctly ported'"

[Eric Wieser]

I mean that they had alignment warnings until we turned those off

[Mario Carneiro]

alignment warnings don't affect the #print correctly_ported /-- ... thing

[Mario Carneiro]

the point is not really to assert that the result is correct, but rather just that the declaration has already been aligned to an existing theorem

[Eric Wieser]

My understanding was that the #print was only emitted if there is no alignment warning

[Mario Carneiro]

no, the #print is emitted if the declaration is aligned (manually or automatically) to an existing definition

[Mario Carneiro]

no, you are correct, a dubious translation prevents the #print

[Eric Wieser]

In your defense, it probably would have been more useful for me to say nothing until I had the source code for mathport open; but I'm glad to hear I wasn't imagining things.

[Mario Carneiro]

well now mathport aligns with my first assertion

[Mario Carneiro]

I also removed -- mathport name: and include/omit

[Mario Carneiro]

it's still showing #print lines though, there is a config flag for it