Mathlib/* labels

Stream: mathlib4

[Joseph Myers]

I noticed that #34393 has a new label "Mathlib/Geometry/Polygons" which was apparently added by a bot. It seems we also have a "Mathlib/CFT" label with no PRs currently associated with it. What is the purpose of these labels, which seem very stylistically different from all the other labels we currently use, and what is the logic the bot uses to add them?

[Yaël Dillies]

Mathlib/CFT sounds like a botched version of the CFT label

[Jon Eugster]

This is a bug in the autolabelling bot:

Screenshot 2026-01-25 at 23.59.20.png

Although not sure why it does this... I'm looking into it, maybe I can push a fix for this to #34066 before it gets reviewed

[Jon Eugster]

Ah no, the autolabel script works as expected, it's the github action which fails. Particularly the line

label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')"

(Link to source) This got introduced in #25641 (link to commit).

@Damiano Testa you probably know better what motivated this PR, could I leave it for you to fix?

[Jon Eugster]

(I've deleted the bad labels now. Reproduction: when a PR adds a new folder outside any label, the autolabel script returns an empty array, but also a warning like "the following paths are not covered by any label #[Mathlib/Geometry/Polygon]". The linked sed then mistakenly parses this and thinks it should add Mathlib/Geometry/Polygon as a label.)

[Violeta Hernández]

This same Polygon label got added in #34566, which has nothing to do with polygons.

[Damiano Testa]

Ok, thanks for the reports and diagnostics!

[Damiano Testa]

As far as I understand, there are two somewhat unrelated issues.

1. The new Polygon directory exposed a gap in the autolabel coverage and the script has been correctly picking this up.

   A fix for this, is to make autolabel apply the appropriate label to changes in this dir, which could happen with the revamp in #34066 or in a separate, much smaller PR.

2. The mechanism that retrieves the output of lake exe autolabel and decides if a unique label is applicable mistakenly reads the "gap in autolabel" report as a label to be added and uses that to label PRs.

   I'll think about a fix for that and will produce a PR.

[Damiano Testa]

If I remember correctly, there had been a discussion of having the action post a message on Zulip when it noticed a gap in autolabels. Maybe this is a good time to think about doing that as well.

[Damiano Testa]

#34568 (the previous PR was entirely an arithmetic progression!)

[Damiano Testa]

The PR above should restore the correct functionality of autolabel. It does not address the fact that Polygon still produces warnings.

[Jon Eugster]

Damiano Testa said:

A fix for this, is to make autolabel apply the appropriate label to changes in this dir, which could happen with the revamp in #34066 or in a separate, much smaller PR.

I think I'd prefer a follow-up PR which just adds the Polygon dir to the list. I can create that once #34066 lands. (or it can happen earlier, then I just need to make sure the refactor PR is updated correctly)

[Jon Eugster]

(made a PR to add then new Mathlib/Geometry/Polygon: #34677)