Suggestions for #port-dashboard

Stream: mathlib4

[Moritz Firsching]

Eric Wieser said:

Jakob von Raumer said:

Having the PR tags on mathlib-port-status would be a cool feature, to quickly see where help is needed

PRs to https://github.com/leanprover-community/mathlib-port-status are welcome :).

https://github.com/leanprover-community/mathlib-port-status/pull/2

[Yury G. Kudryashov]

Also, it would be nice to ignore default.lean files on https://leanprover-community.github.io/mathlib-port-status/old

[Eric Wieser]

Moritz Firsching said:

Eric Wieser said:

Jakob von Raumer said:

Having the PR tags on mathlib-port-status would be a cool feature, to quickly see where help is needed

PRs to https://github.com/leanprover-community/mathlib-port-status are welcome :).

https://github.com/leanprover-community/mathlib-port-status/pull/2

This is now live:

image.png

[Johan Commelin]

Really nice! And very useful!
One minor issue: the yellow labels are really hard to read

[Eric Wieser]

Yeah, ideally we'd copy the CSS from github which has a bunch of computation to choose appropriate transparency / text color

[Eric Wieser]

PRs remain welcome, but I figured getting ugly labels merged ASAP was better than waiting for pretty labels

[Heather Macbeth]

Can we please have it on https://leanprover-community.github.io/mathlib-port-status/old too?

[Eric Wieser]

That's a bit harder because the code that generates old throws away the PR number information

[Eric Wieser]

(instead it keeps around some plaintext that sometimes contains mathlib4#...)

[Ruben Van de Velde]

While you're there, do we need the PR number twice for all the in progress files?

[Eric Wieser]

That's a bug in https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/file_status.py

[Eric Wieser]

It computes comments incorrectly

[Notification Bot]

24 messages were moved here from #mathlib4 > port progress by Eric Wieser.

[Eric Wieser]

I added a diagram to explain a little better what's going on at https://github.com/leanprover-community/mathlib-port-status/blob/main/README.md

[Eric Wieser]

Ideally we would eliminate run_port_status.sh and have port_wiki be an output of mathlib-port-status

[Moritz Firsching]

Johan Commelin said:

Really nice! And very useful!
One minor issue: the yellow labels are really hard to read

https://github.com/leanprover-community/mathlib-port-status/pull/5
I tried to do approximately what is done on github regarding the color of the text of the labels...
bwlabels.png

[Moritz Firsching]

Heather Macbeth said:

Can we please have it on https://leanprover-community.github.io/mathlib-port-status/old too?

Really seems like this is slighly harder to do. Is there something that can be improved in the new port status change to make it more useful for you?

[Heather Macbeth]

@Moritz Firsching Thanks! Yes, I'd like the categorization on "new" port-status to be the same as the categorization on "old" port-status, with the first category to be "ready-to-port" (defined as "all dependencies ported", whether or there is an open PR).

[Johan Commelin]

@Heather Macbeth can you explain why?

[Johan Commelin]

Currently, I find the top 10 of the top two categories in "new" quite useful

[Johan Commelin]

The first one shows the top 10 ports that are in progress, the second one the top 10 that are ready to be ported

[Johan Commelin]

(Both are (default) sorted by the number of files that depend on that item, which is the most useful sort in my opinion.)

[Ruben Van de Velde]

Should port-status also show counterexamples/archive?

[Heather Macbeth]

In my opinion, we want to encourage people to think of the "ready-to-port" (all dependencies ported) files as a unit, and to jump in on the highest priority ones whether there's an open PR that needs extra hands or a file which needs a PR to be started. It's hard to judge the relative importance of two such files when they are not on the same list (I have to read and compare the number of dependencies).

[Johan Commelin]

@Ruben Van de Velde I guess we can add those, but it's not high priority. All those files are leaves of the import tree.

[Eric Wieser]

Does mathlib3port even include countexamples/archives?

[Eric Wieser]

A weak argument for separate tables is that some columns only make sense for things with a PR

[Heather Macbeth]

If someone is scanning through a table of "ready-to-port" files, they will still want to be able to see which ones have PRs open and which don't, so the (fairly narrow) columns for PR number and labels convey information even when they're empty.

[Jireh Loreaux]

I think I prefer Heather's format if and only if we can separate out files we want to ignore into a separate list (e.g., .default or other things we decide we're not going to port). This already clutters the "ready to port" list.

[Eric Wieser]

Ideally #port-comments would have a boolean not_for_porting flag

[Eric Wieser]

@Johan Commelin, if I make a change to https://github.com/leanprover-community/mathlib4/blob/master/scripts/run_port_status.sh willl your server pick it up automatically?

[Johan Commelin]

@Eric Wieser usually

[Eric Wieser]

Eric Wieser said:

Ideally #port-comments would have a boolean not_for_porting flag

Now done, this contains a should_port: false

[Eric Wieser]

Ruben Van de Velde said:

While you're there, do we need the PR number twice for all the in progress files?

Fixed by not using mathlibtools any more, and instead getting the data from the new more structured yaml file. The readme diagram has been updated to explain the added spaghetti.

[Johan Commelin]

@Eric Wieser should the port-graph-bot (PDFs) and port-progress-bot (stats) also be added to that diagram?

[Johan Commelin]

They need mathlibtools and hence the old wiki-yaml file...

[Eric Wieser]

Yes

[Eric Wieser]

But I don't know enough about them to add that

[Eric Wieser]

Feel free to push changes to the readme, you can preview the graphvis-ish syntax on the GitHub web editor

[Johan Commelin]

@Eric Wieser https://github.com/leanprover-community/mathlib-port-status/pull/8 but it doesn't compile.

[Eric Wieser]

I think graph is a reserved word for the node id

[Johan Commelin]

So, what does mermaid suggest? That we write garph or grahp instead?

[Yakov Pechersky]

graf, or in "klass"ic python style, graph_

[Eric Wieser]

It's just a node id, it doesn't matter what you write as it doesn't appear in the output

[Eric Wieser]

I pushed a fix, but the node text doesn't make any sense at the moment as it assumed that the node id was also rendered

[Eric Wieser]

The "possibly out of sync" file list is now sortable by number of out-of-sync mathlib3 PRs, and by size of diff:

image.png

[Johan Commelin]

Great! Do the "green plus" and "red minus" just mean expand/collapse?

[Johan Commelin]

Ok... I was hoping it was some magic prediction about how much effort it was to sync the file :rofl:

[Eric Wieser]

It is; the prediction is "oh it's easy" until you see the diff, then its "oh, this is harder"

[Johan Commelin]

Thanks for building this tooling!

[Eric Wieser]

I think this tooling isn't enough to start working through the list, but it's probably enough to help work out what tooling we really need; but let's have that discussion in this thread.

[Eric Wieser]

I've made some tweaks to the dependency graphs now; see port-status#data/complex/basic. Better before

image.png

or after? (live at the moment)

image.png

[Ruben Van de Velde]

What do all the colors mean?

[Eric Wieser]

They're just to help you follow the lines

[Eric Wieser]

(but also they're just the default behavior in the template I copied)

[Eric Wieser]

Maybe I should do that with hover behavior instead

[Mario Carneiro]

yeah the colors are misleading

[Eric Wieser]

Is there any point showing the ported ancestors on the graph anyway?

[Eric Wieser]

Oh, I tricked myself into thinking that #mathlib4 > port progress does it, but it doesn't

[Reid Barton]

it used to

[Eric Wieser]

Ok, colors removed; now looks like this

image.png

[Yury G. Kudryashov]

@Eric Wieser https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot shows "last sync" at 995b47e5 but it also shows !4#2406 mathlib 4 commit which changed the mathlib 3 commit to afdb4fa3

[Yury G. Kudryashov]

Did I do something wrong in !4#2406?

[Eric Wieser]

Last sync refers to the yaml file

[Eric Wieser]

Which can be a few minutes behind

[Yury G. Kudryashov]

Merged 13h ago

[Eric Wieser]

I think the yaml file is having caching problems

[Eric Wieser]

@Johan Commelin reported this to me privately a few days ago for something unrelated

[Yury G. Kudryashov]

BTW, !4#2498

[Eric Wieser]

@Yury G. Kudryashov, that PR forward-ports changes that @Yaël Dillies and I already had forward-port PRs open for

[Eric Wieser]

I think reviewing existing forward-ports should take priority over trying to find things that we forgot to forward port

[Yury G. Kudryashov]

I'm sorry. These files were not highlighted as "in progress" on https://leanprover-community.github.io/mathlib-port-status/out-of-sync , so I assumed that it's safe to deal with them.

[Eric Wieser]

"in progress" means "a PR with an initial port of a file is already out of date even though it's not merged yet"

[Eric Wieser]

Evidently I need to use a less confusing label for it

[Yury G. Kudryashov]

Can you list PRs that touch the ported file if there are any?

[Eric Wieser]

See the discussion in this thread.

[Eric Wieser]

Done, thanks @Jon Eugster!

[Jireh Loreaux]

@Eric Wieser There's a bug somewhere with the port status page. Right now it lists data.mv_polynomial.{basic, rename, monad} all with the PR data for monad only.

[Jeremy Tan]

The same happens with linear_algebra.affine_space.affine_equiv and the two PRs depending on it. The bug's been there for a while

[Yury G. Kudryashov]

I guess, it lists a random PR that adds this file.

[Eric Wieser]

There is an open issue about this I think. The port yaml file confuses dependent PRs.

[Johan Commelin]

You need an algorithm that looks at a PR and decides which file(s) it is adding, and then find a partial inverse to that map.
The current algorithm is certainly not doing a great job at that...

[Eric Wieser]

A simple fix might just be to have a one-to-many mapping between files and PRs

[Eric Wieser]

Then the algorithm can run in the head of the human reading the page

[Jireh Loreaux]

Since PR titles for ported files are generated by the script, why not just use the name in the title? Ultimately if this is just for dependent PRs it's not that important though.

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/blob/master/scripts/make_port_status.py is the script that would need to change

[Johan Commelin]

Jireh Loreaux said:

Since PR titles for ported files are generated by the script, why not just use the name in the title? Ultimately if this is just for dependent PRs it's not that important though.

The problem is that dependent PRs hijack the entry of the non-dependent PR on the port status dashboard.

[Johan Commelin]

I think using PR titles might be more robust. But they are not all formatted in the same way. So it would require a bit of string-fu.

[Eric Wieser]

Picking early PR numbers over later PR numbers would probably be enough in 90% of cases

[Joël Riou]

Currently the first "unported file" in the port status page appears to be algebra.category.Mon.basic, but it is ported at !4#2902 It is due to a renaming s/Mon/MonCat/

[Jeremy Tan]

Joël Riou said:

Currently the first "unported file" in the port status page appears to be algebra.category.Mon.basic

Probably have the PR actually merged, and then it'll jump from unported to ported?

[Eric Wieser]

Hmm, that is weird; it should definitely show up in the "in progress" section

[Eric Wieser]

https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status says "No", so the fault is not the dashboard but the script generating its data

[Eric Wieser]

I think the script is using filename heuristics instead of reading the source header, which is obviously not the right thing to do

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/pull/3015 might fix it; mind testing @Johan Commelin?

[Johan Commelin]

Running a test...

[Johan Commelin]

@Eric Wieser done. Please let me know whether you are happy with the output

[Johan Commelin]

looks like it's working

[Eric Wieser]

algebra.category.Mon.basic is still 'no' on the port wiki

[Eric Wieser]

I guess the cron job rolled back your test?

[Eric Wieser]

(I was in a meeting, sorry)

[Johan Commelin]

yes, presumably the cron-job undid my test.

[Johan Commelin]

But #port-dashboard looks fine (because it has 30m builds, instead of 5m builds)

[Eric Wieser]

Oh, did you change the frequency of the cron job?

[Eric Wieser]

I agree it looks fine though; if this was going to fail, the failure mode would have been a totally empty list of "in progress" PRs

[Jeremy Tan]

There's a nonexistent file currently showing as unported on the mathlib porting status page, algebra.monoid_algebra.division

[Matthew Ballard]

I think you have to wait for mathport to run on that

[Eric Wieser]

Yes, I only just created that file. port-status#algebra/monoid_algebra/division

[Eric Wieser]

I've now added a comment telling you not to port it yet :)

[Jeremy Tan]

Now there's a backlog of awaiting-review PRs, some of which will clear the way for even more files to be ported...

[Eric Wieser]

Eric Wieser said:

I've now added a comment telling you not to port it yet :)

It's worth noting that while it appears right at the top of the dashboard, it's not actually blocking anything at all

[Eric Wieser]

Because the file that imports it in mathlib3 doesn't import it (yet) in mathlib 4

[Matthew Ballard]

Is that file ported/under porting?

[Matthew Ballard]

To answer my own question, no I can't read

[Eric Wieser]

There are two files that imports it; one is a leaf, and the other is already ported

[Matthew Ballard]

I guess I can't read.

[Ruben Van de Velde]

I wonder if the graphs could highlight the root nodes as well - right now they can be easily missed in the tangle. For example, matrix.to_lin is one here:

Screenshot-from-2023-04-20-13-35-30.png

(second box under polynomial.quotient on the right)

[Eric Wieser]

That's a good idea

[Eric Wieser]

port-status#ring_theory/algebraic#graph

[Eric Wieser]

On the other hand, its position tells you that we shouldn't worry about it nearly as much as the other nodes :)

[Eric Wieser]

@Eric Rodriguez, if you wanted to cleanup the docstrings in to_lin before porting, I recommend you do so soon!

[Ruben Van de Velde]

Too late :)