Out of sync files

Stream: mathlib4

[Eric Wieser]

Reposting another thread, https://leanprover-community.github.io/mathlib-port-status/out-of-sync now includes the output of the diff and list of relevant PRs. I think we probably need some more information to start clearing out this list, perhaps:

• Links to the relevant mathport output
• Diff in mathlib4 between the initial port and the one at HEAD
• Difference in #align data?

(note I renamed the topic, since the old title referred to a header that was renamed on #port-status)

[Eric Wieser]

I've made a bit more progress on this; port-status#topology/constructions now shows:

• The mathlib4 changes too
• The mathlib3 changes which claim to have been ported

This is important because that file claims to have forward-ported something it has not!

[Yury G. Kudryashov]

docs4#Int.cast_natAbs and docs#int.cast_nat_abs have different RHS

[Yury G. Kudryashov]

I can fix it tomorrow unless someone fixes it today.

[Eric Wieser]

@Mario Carneiro, how hard would it be for you to modify mathport to output "dubious translations" into a json file?

[Mario Carneiro]

What format?

[Mario Carneiro]

also it will probably be a bunch of json files, not just one

[Yury G. Kudryashov]

Am I right that there are some false positives because of the changes in typeclasses?

[Eric Wieser]

Although I guess it wouldn't be useful, since the error we care about here is made invisible by all the false positives in the rest of the file

[Mario Carneiro]

what makes them FPs?

[Eric Wieser]

Mario Carneiro said:

also it will probably be a bunch of json files, not just one

Sounds fine to me. I think any json format containing:

• mathlib3 filename
• mathlib3 decl name
• mathlib4 decl name
• the two types from the error message

would do the trick. Including the mathlib3 / mathlib4 shas in the json file (if they're not already elsewhere in the mathlib3port repo) might be good too.

[Eric Wieser]

Mario Carneiro said:

what makes them FPs?

At a glance it looks like they're complaining about syntactically different but defeq ways of constructing TC instances

[Eric Wieser]

Which is particularly unfortunate, because probably the most common mistake is going to be getting coercions in the wrong place because elaboration order changed, but we're pretty much guaranteed a FP on any lemma containing a coercion that's correctly ported

[Yury G. Kudryashov]

Some sources of what I would call false positives:

• coe vs a function;
• bit0 (bit1 0) vs 2
• non-aligned instances (we rarely #align them)

[Yury G. Kudryashov]

BTW, could you please change standalone coes to (↑) in mathport?

[Eric Wieser]

Point 3 sounds like an argument in favor of aligning them

[Yury G. Kudryashov]

Am I right that it's hard to generate #align lines in mathport because it's hard to predict Lean 4 names?

[Yury G. Kudryashov]

I wouldn't bother about aligning instances before we deal with coe vs function.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

what makes them FPs?

At a glance it looks like they're complaining about syntactically different but defeq ways of constructing TC instances

No, this is an artifact of the printout. If it reports an error then they are really not defeq, but there might be a bunch of other defeq things that make it hard to see the part that isn't defeq just via diffing

[Eric Wieser]

Can the error message be adjusted to distinguish "not defeq" from "declarations don't exist", which is I assume what what the docs4#Int.instRingInt / Int.ring complaints are about?

[Mario Carneiro]

no, in both cases all the declarations exist

[Mario Carneiro]

it wouldn't even make sense to ask for defeq if the declarations are missing

[Mario Carneiro]

In most cases those declarations that you can't find were previously generated by mathport itself when processing the upstream file

[Mario Carneiro]

this happens a lot for instances because instances don't get #align statements

[Mario Carneiro]

aligning instances may silence a lot of these errors, if those instances are in fact not defeq

[Jon Eugster]

From my recent test to update some out-of-sync files, I think it would be useful to have an option to sort them by import order. Here's a suggestion PR to mathlib-port-status.

screenshot_port_status.png

[Eric Wieser]

Thanks for the PR! I've left some comments.

[Eric Wieser]

An unrelated missing feature is that we have no easy way of seeing if a resync PR already exists

[Eric Wieser]

That's not a particularly challenging problem to solve (just crawl all the files in PRs with the "pair" label too), but needs time from someone.

[Eric Wieser]

This is now live, thanks @Jon Eugster (and @Jireh Loreaux for another change on #port-dashboard)

[Jon Eugster]

Eric Wieser said:

An unrelated missing feature is that we have no easy way of seeing if a resync PR already exists

mathlib-port-status#15
mathlib-port-status#16

[Eric Wieser]

I'm not too happy with adding more GitHub API calls to that page; I'd prefer it if we could get the API calls out of the way up front (i.e. by getting the forward-port PRs in the yaml file; or maybe with a two-phase build)

[Eric Wieser]

(part of the reason is that API calls are a pain to test due to rate limits)

[Jon Eugster]

Eric Wieser said:

I'm not too happy with adding more GitHub API calls to that page; I'd prefer it if we could get the API calls out of the way up front (i.e. by getting the forward-port PRs in the yaml file; or maybe with a two-phase build)

API rate limits are a bit of a pain indeed, having to set GITHUB_TOKEN etc... The two options you mentioned:

• If we added these API calls to make_port_status.py (L. 117) instead (which creates the yaml file), would that improve anything in your view?
• We could move these API calls together with the ones for the PR-labels on #port-dashboard to a separate file next to make_html.py. And then save the output as temporary file somewhere. That way you could skip the API calls completely during testing.

What would you prefer?

[Eric Wieser]

The first option sounds easier (and was what I had planned to do)

[Eric Wieser]

Eliminating the need for make_port_status via the second option would also be nice though

[Eric Wieser]

The only slight difficulty is that to fully replace that script we need to upload to the github wiki

[Eric Wieser]

And that requires a stronger token than I'm willing to grant from my personal account

[Eric Wieser]

Jon Eugster said:

Eric Wieser said:

An unrelated missing feature is that we have no easy way of seeing if a resync PR already exists

mathlib-port-status#15

Looks like you clobbered these changes by force-pushing a different branch on top of them

[Jon Eugster]

apparently :woozy_face: (mathlib-port-status#16)

[Eric Wieser]

The dashboard now shows the mathlib3port output, for the sake of forward-porting; see port-status#algebra/star/self_adjoint for an example

[Eric Wieser]

(deleted)