Uploading the import graph

Stream: mathlib4

[Julian Berman]

I want (a topologically sorted) import graph for mathlib, which I know importGraph basically generates. I see Mathlib's CI runs generate this, but it appears just to confirm the command works, then they immediately throw the data away. Unless I'm missing somewhere else which does this, is there any objection to preserving the graph on build? #19162 is a PR which does so if not.

[Julian Berman]

I guess now that I see it in the comment, this I think means scripts/count-trans-deps.py could operate on the import graph file rather than custom-parsing Lean code, though if it works at the minute of course who cares.

[Julian Berman]

(CC @Kim Morrison @Damiano Testa )

[Damiano Testa]

I do not know how the GitHub API quota works, but I know that Mathlib is often running out. Does this step add extra burden on this?

[Damiano Testa]

Alternatives could be to run it on a schedule, maybe once a day on master?

[Damiano Testa]

Or rather than saving it as an artifact, just printing the resulting dot file and store it in the CI logs?

[Damiano Testa]

As I mentioned, my main concern is the API quota, and I'm not sure of what is "lighter" from this perspective.

[Julian Berman]

Do you know which quota Mathlib tends to use up? I suspect it's the minutes quota maybe? I don't think I can see that data, but will double check. (If that's the one, this wouldn't put more pressure on it -- it does use up a bit of the storage quota, but AFAIK the "real stuff" stored, i.e. oleans, are not using GH Actions storage, they are in some cloud bucket?) But it's definitely a good thing to double check.

[Julian Berman]

Oh fun, I can indeed see https://github.com/leanprover-community/mathlib4/actions/metrics/usage, that's new.

[Bryan Gin-ge Chen]

We don't use any "minutes", I don't think. It's mainly the GitHub API quota in e.g. the GITHUB_TOKEN provided to github actions that we've been concerned about lately.

[Julian Berman]

Aha.

[Julian Berman]

From rate limiting? Or literally hitting the limit in some period?

[Bryan Gin-ge Chen]

Yeah, we've had issues with hitting the limit before so we have been using personal tokens from various "bot" accounts.

[Julian Berman]

Got it. OK, that does sound like a concern then. Hm.

[Bryan Gin-ge Chen]

I just found this discussion about upload-artifact, which suggests that it might be using a separate quota: https://github.com/actions/upload-artifact/issues/197

If that's true then I see no objection to your PR.

[Julian Berman]

Fun, I didn't know that myself.

[Damiano Testa]

Ok, I'm glad that we checked! I'm happy to try it out and, potentially, revert it if it causes problems and think of alternatives!

[Damiano Testa]

Bryan, are you happy with this as well?

[Bryan Gin-ge Chen]

Sure, let's go for it.

[Damiano Testa]

I just put it on the queue!