setting up a working copy of Mathlib in CI

Stream: Is there code for X?

[Damiano Testa]

There are a couple of CI workflows that set up a working copy of Mathlib with cache. Is there a way to make all the steps that lead up to that into a single action, so as to avoid repetition and clutter?

[Damiano Testa]

My reason for asking is that I would like to set up yet another such workflow and it seems very brittle to copy paste the same steps once again.

[Johan Commelin]

I think someone suggested that we should have a github repo leanprover-community/gh-actions that would provide a bunch of common actions that mathlib CI and dependent projects could then reuse.

[Johan Commelin]

I have no idea how to set this up, but I do think it is a great idea.

[Yaël Dillies]

My understanding of actions is that you need one repo per action

[Damiano Testa]

Oh, so this means that I could create a repo on my github account, use it for the workflow for the weekly reports and then, when/if mathlib wants to have one, I could switch to using that, right?

[Damiano Testa]

(My repo would essentially be copy-pasting the current CI steps that create a working copy of mathlib and all the fluff that needs to be added to make it into an action and that I will ask chat-gpt about...)

[Damiano Testa]

Btw, according to this section, it is recommended that actions be in their own repo. This seems to imply that it is not required, but I am really just reading on this for the first time now.

[Kim Morrison]

Johan Commelin said:

I think someone suggested that we should have a github repo leanprover-community/gh-actions that would provide a bunch of common actions that mathlib CI and dependent projects could then reuse.

Such an action now exists and is being used in some repositories. I'm away from the computer right now, but search for lean-action here in zulip and you should find it.

[Damiano Testa]

I Imagine that this is a thread discussing the action.