non-aligned definitions

Stream: mathlib4

[Yury G. Kudryashov]

Is it hard to generate the list of definitions that are in ported files but neither aligned, nor noaligned?

[Yury G. Kudryashov]

Probably, we should skip instances.

[Floris van Doorn]

Oh that would be nice. And maybe add a linter for this...

[Reid Barton]

Do you mean definitions in the corresponding Lean 3 files?

[Reid Barton]

(I think so because #noalign only involves a Lean 3 identifier)

[Floris van Doorn]

Oh wait, I meant a Lean 4 linter, but that's not the most logical direction. We could still lint for declarations that have no aligned Lean 3 declarations to it, but that will have (many?) false positives.

[Reid Barton]

Yes I think we would need something that has access to both mathlib3 and mathlib4.

[Eric Wieser]

A CI job that does that comparison is the kind of thing I was hoping we could host in the mathlib-port-status repo

[Yury G. Kudryashov]

IMHO, both parts of the "API diff" are useful.

[Reid Barton]

https://gist.github.com/rwbarton/e604a3d06300a0fc31e31276b055403b

[Reid Barton]

Missing aligns = definitions in the original files that don't have corresponding #align statements
Phantom aligns = #align statements about Lean 3 definitions that don't exist (usually because the name is incorrect somehow)

[Reid Barton]

Currently, 6061 entries total

[Eric Wieser]

Can you commit the script you used to generate that to the mathlib-port-status repo? It doesn't need to be set up to do anything in CI (yet)

[Reid Barton]

There are a few (< 100) that are #noaligned, those should not be in the list.

[Reid Barton]

https://github.com/leanprover-community/mathlib4/tree/align-aligns but it relies on some manual input for now

[Reid Barton]

I guess this list will keep people busy for a while

[Reid Barton]

I'm going to take a whack at some of the "phantom aligns" :locked:

[Reid Barton]

https://github.com/leanprover-community/mathlib4/pull/1794

[Reid Barton]

:unlocked: but I did pretty much all of them, I only ignored some that were clearly do to unsynchronized mathlib 3 changes (uIcc etc)

[Reid Barton]

It would be a big help if it was an error to put a capital letter on the left side of #align.

[Mario Carneiro]

Sure, let's do that. mathlib4#1796

[Mario Carneiro]

I implemented the linter but it's probably best for someone else to handle reviewing all the linter postives and ignoring or fixing them as appropriate

[Reid Barton]

hmm right

[Reid Barton]

there's also some small number of actual capital letters in mathlib 3

[Reid Barton]

I guess those we handle with nolint?

[Mario Carneiro]

I'm imagining you would use set_option linter.uppercaseLean3 false either immediately before the affected #align statement or at the top of the file / in a section if it concerns a whole sequence of theorems

[Mario Carneiro]

(this is a lean 4 style linter not a mathlib linter)

[Reid Barton]

Is the file export.json produced by doc-gen served directly from somewhere?

[Reid Barton]

https://gist.github.com/rwbarton/e604a3d06300a0fc31e31276b055403b updated for today

[Eric Wieser]

It's available for download from the GitHub actions jobs

[Reid Barton]

Yeah, I was hoping for something in a fixed location

[Reid Barton]

It is not clear to me how to get the latest version automatically, since the job does not always upload it (I guess if nothing changed?)

[Eric Wieser]

Oh, can you use decls.bmp for what you need?

[Reid Barton]

I have no idea

[Reid Barton]

because I don't know what that is

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs/searchable_data.bmp

[Eric Wieser]

It's secretly a json file, but github doesn't gzip it unless we pretend it's a bitmap

[Reid Barton]

I'm using some of the other fields too (notably filename, but also is_meta, attributes)

[Eric Wieser]

Then I think the answer is probably "modify doc-gen so that it publishes export.json to the webpage"

[Eric Wieser]

Although it might be too big for that in the current deployment mechanism (committing the outputs to git), in the same way the the Lean web editor was

[Eric Wieser]

Now that, by-file, the port is 100% complete, it might be worth doing another check of the aligns to check we've done a reasonable job by-definition

[Yury G. Kudryashov]

docs3#option.get_or_else_some is not aligned

[Eric Wieser]

Pretty much everything in core: init isn't, apart from the ones I assume mario did by hand

[Mario Carneiro]

at that time the convention was to add aligns only when the auto naming convention didn't get the right answer

[Eric Wieser]

Can we teach #lookup3 that convention?

[Eric Wieser]

How hard would it be to teach mathport to dump a json along the lines of:

{"mathlib3_name":
   {"existsInML3": true,
    "info": {
        "instance": false,
        "meta": false,
        "ml3_file": "mathlib3.import"
    },
    "aligned_with": $RenameMap.toLean4},
   ... }

[Eric Wieser]

Obviously RenameMap is trivial to get from lean4 alone, but the extra lean3 metadata either requires me to run lean3 too, or to extract it from mathport

[Yury G. Kudryashov]

option.get_or_else_some is in data.option.basic and it is not auto aligned to Option.getD_some. I'll open a PR later today. Do we have a list of Lean 3 definitions/lemmas that are not #aligned?

[Eric Wieser]

I was hoping that Mario could produce a nice json file to analyze to save me getting lean3 and lean4 CI co-existing in mathlib-port-status...

[Mario Carneiro]

that's mathport-lint, a project I have been meaning to work on for a while. There is stuff that requires accessing the olean files generated by all of mathport (i.e. Mathbin.olean), which is currently not saved and only exists in CI. So we could add another step after that data is generated to construct some jsons or something

[Eric Wieser]

I'm a bit worried that as soon as we say "mathlib4 is open to refactors" it becomes too late to meaningfully run such a tool