port status

Stream: mathlib4

[Johan Commelin]

FYI https://math.commelin.net/files/port_status.html shows the current output of port_status.py with a little bit of linkification. It is updated automatically every hour.

[Eric Wieser]

Can you linkify the git diff d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..HEAD src/data/int/cast/basic.lean to a diff on github? edit: no, I think no such page exists

[Scott Morrison]

I've updated the linkifiers so #port-status points there, and #port-wiki points to the wiki page.

[Johan Commelin]

Please add free-form comments related to porting mathlib3 files to mathlib4 to the following wiki page
https://github.com/leanprover-community/mathlib4/wiki/port-comments

The port-status.yaml wiki page can still be used to switch status from No to Yes etc... but hopefully that will be done automatically in 3~4 hrs from now.

[Johan Commelin]

Remarks:

1. This file is hosted on the mathlib4 wiki, instead of mathlib3
2. :notifications: :warning: Free-form comments that are added to port-status.yaml on the mathlib3 wiki will get lost once a bot starts taking care of that file.

[Reid Barton]

The old port status wiki page (hosted on the mathlib3 wiki) is now read-only.
(It will be updated automatically by a script, based on the current status of PRs, so that existing tools that depend on this page will continue to work.)

As Johan said above, if you want to add free-form comments about files that don't have PRs yet,
edit https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit instead.

[Reid Barton]

In particular, this means you no longer have to record any information on that page when opening or when merging a PR.

[Eric Wieser]

Where does the machinery for doing this automatically live now?

[Reid Barton]

On my office computer ...

[Ruben Van de Velde]

I hope your office isn't shutting down for the new year :)

[Eric Wieser]

Can we move it to github actions so that it can be community maintained?

[Eric Wieser]

Either inside mathlib4, or a new mathlib-port-status repo which could also generate static status pages at leanprover-community.github.io/mathlib-port-status

[Reid Barton]

Sure, but it would first have to attain a more complete form of existence

[Anatole Dedecker]

Do I understand correctly that we lo longer have to provide any commit-SHA infos anywhere? All instructions about it got removed from the wiki page

[Reid Barton]

Yes, that's correct (because the information is in the header of the mathlib4 files)

[Eric Wieser]

What's our workflow for updating mathlib4 files after a mathlib3 PR now?

[Eric Wieser]

Let say @Yaël Dillies and I both modify different bits of a mathlib3 file that's ported to mathlib4; if we both make PRs to mathlib4 to forward-port our PRs, who updates the SHA, and to what?

[Reid Barton]

I think the easiest way is:
When making a mathlib3 PR, the author should also make a mathlib4 PR with the corresponding changes, but without modifying the header.
Then, at some (hopefully not too much) later point, someone can notice that the mathlib3 file has been updated since the version specified in the mathlib4 header, look at the changes made to the mathlib3 file since that version, verify that they have also been made on the mathlib4 side (or update the mathlib4 side if not), and then commit a mathlib4 change updating the header.

[Reid Barton]

There was already basically the same kind of process necessary when updating the SHAs on the wiki page (which I think mostly hasn't been happening at all).

[Johan Commelin]

@Scott Morrison discovered a "bug" in the current set-up. If you create a PR for porting a file that already had a partial-ad-hoc port, then the current system does not recognize this, and does not automatically list that PR in #port-status. It will also not be taken into account in the progress reports/graphs.
To remedy this, for these edge cases we should manually register the PR at the start of a free-form comment in https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit

[Eric Wieser]

Something seems to have gone wrong with the yaml file at #port-wiki: the bot is renumbering PRs like crazy in https://github.com/leanprover-community/mathlib/pull/17979

[Eric Wieser]

I would guess it's the removal of the quotes

[Scott Morrison]

@Eric Wieser, you're proposing that @Reid Barton should add triple backticks before and after the comment block at the top of the file?

[Scott Morrison]

Could you remind me why the synchronization-warning bot cares about this?

[Eric Wieser]

Maybe; or maybe the problem is the single quotes

[Eric Wieser]

The synchronization bot is just using the mathlibtools API

[Eric Wieser]

Which it seems is no longer parsing things properly

[Eric Wieser]

Ok, my re-diagnosis is that there is no formatting issue after all; it seems @Reid Barton has somewhat rewritten history and declared that the PRs which ported the files are not the same ones that were previously claimed

[Eric Wieser]

e.g. that algebra.group.defs was ported in mathlib4#4 not mathlib4#457

[Eric Wieser]

Which is to say; it's recording the ad-hoc ports not the real ports

[Scott Morrison]

Not ideal, but not a total disaster?

[Eric Wieser]

Let's refrain from merging #17979 until we're sure this was deliberate

[Eric Wieser]

I'd argue that if we're going to reference ad-hoc ports in the PR number, there's little point mentioning the PR at all

[Eric Wieser]

(some PRs seem to have been dropped entirely too)

[Reid Barton]

Oh yeah it's definitely semi-intentional, that we did not bother to retain the correct PR number in all cases

[Heather Macbeth]

I notice that mathlib4#1052 is not listed as an open PR for logic.equiv.local_equiv; is this deliberate for some reason?

[Reid Barton]

This is because the PR doesn't add a file, due to an ad-hoc port

[Heather Macbeth]

Perhaps we could temporarily solve this by writing a comment in the porting wiki? (Same for data.rat.defs and data.fin.basic.)

[Reid Barton]

I just added a line to https://github.com/leanprover-community/mathlib4/wiki/port-comments for it

[Reid Barton]

Yes, please go ahead and add similar lines for those.

[Reid Barton]

Basically, the ad-hoc ports cause many headaches which we hope will disappear on their own fairly soon.

[Reid Barton]

I didn't realize that the SYNCHRONIZED comments in mathlib3 mention a PR number, or that the bot would try to rewrite an existing comment; probably fixing the latter is easiest

[Reid Barton]

A few files like Data.Char mentioned above are missing any PR number because they were not even created by a PR in the first place

[Heather Macbeth]

Any idea why mathlib4#888 doesn't show up for order.hom.bounded? Judging from the PR, it doesn't seem to replace an ad-hoc file.

[Reid Barton]

That's because it is based on a too-old mathlib3port, and is missing the header information about what mathlib3 module/version it is based on

[Reid Barton]

https://github.com/leanprover-community/mathlib4/labels/no-source-header
these PRs should have those headers added, and then the label removed

[Scott Morrison]

I've add the source headers and removed the labels for all but one:

https://github.com/leanprover-community/mathlib4/issues?q=is%3Aopen+sort%3Aupdated-asc+label%3Ano-source-header+

For that one, we need @Moritz Doll to provide a git sha.

[Eric Wieser]

Should we just teach the bot not to mention a PR number at all, either in the description or the comments?

[Eric Wieser]

I didn't realize that the bot would try to rewrite an existing comment; probably fixing [this] is easiest

This was a deliberate choice, the intent was for the yaml to be the source of truth so that we could correct typos and regenerate the headers. It also means we can change the format without discarding data.

[Reid Barton]

Yeah I don't see why it is useful to link to a (closed!) PR at all, really

[Reid Barton]

More useful might be a link to the corresponding file?

[Eric Wieser]

Linking to the closed PR in the commit message is nice because it creates a backlink from the port PR confirming that the marker is in place

[Reid Barton]

That doesn't really seem terribly relevant, since (by assumption) the PR will have been closed by then anyways

[Heather Macbeth]

I notice that data.rat.defs is still marked as unported on #port-status. Maybe it's because it doesn't have the official header?
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Rat/Defs.lean

[Johan Commelin]

Oops!

[Johan Commelin]

I should have caught that while reviewing

[Johan Commelin]

I really hope that we're out of this transitional phase soon.

[Johan Commelin]

And to answer your question: yes, the tooling thinks that this is an ad-hoc port, because the header is missing.

[Johan Commelin]

Fixed in https://github.com/leanprover-community/mathlib4/pull/1122