CI: github-actions bot and module system

Stream: mathlib4

[Michael Stoll]

Is the github-actions bot aware of the module system when it computes the import changes?

In a recent PR (#34533) I added a non-public import to a file, and the bot reported import increases for more than a thousand files. But my understanding is that private imports should not affect the number of files imported in downstream files. Am I wrong, or do we need to fix the bot?

[Bryan Gin-ge Chen]

This is the PR summary bot. @Damiano Testa can probably answer quickly.

[Michael Stoll]

No hurry, I'm just curious.

[Damiano Testa]

The PR summary does not take into account any subtlety introduced by the module system: it simply looks at import statements at the beginning of a file and does its count from there.

[Damiano Testa]

In particular, it does not wait for the oleans to be available, which would be a way to have some module-aware information.

[Michael Stoll]

So I guess that, after introducing the module system, the bot adding the "large-imports" label does not really give useful information anymore? (I.e., it is usually a false positive.)