Can I turn off nightly-testing in my fork?

Stream: CSLib

[Ching-Tsun Chou]

Ever since I pushed a PR:
https://github.com/leanprover/cslib/pull/80
to my fork of cslib yesterday:
https://github.com/ctchou/cslib
I've been getting "run failed" messages like the one shown below. I tried to remove the offending job, but it always came back:
https://github.com/ctchou/cslib/actions/runs/18242962963
How can I turn it off? The failure does not seem to be related to my PR in any way. Thanks in advance!
image.png

[Chris Henson]

In my fork, I was able to click the three dots on the upper right for each job and select "Disable workflow".

[Chris Henson]

We should probably add if: github.repository == 'leanprover/cslib' like other workflows so this doesn't happen for every fork

[Ching-Tsun Chou]

Chris Henson said:

In my fork, I was able to click the three dots on the upper right for each job and select "Disable workflow".

Thanks for the suggestion. I remember I did that on a bunch of jobs yesterday, but I still got failed job notices today. I did it again. Hopefully this will fix itl

[Chris Henson]

You may have been stopping individual runs instead of the whole workflow? It is somewhat confusing to navigate.

[Ching-Tsun Chou]

Not sure. Let's wait and see what happens.

[Ching-Tsun Chou]

Alas, it returned again (see below). I removed all the jobs except the green one (which was triggered by my PR) just half an hour ago.
image.png

[Ching-Tsun Chou]

Another failed run also returned:
image.png

[Chris Henson]

image.png
I don't think you have disabled them. See on the left where they are marked? I did so using the menu on the right.

[Ching-Tsun Chou]

Thanks for the screenshot. I was doing disabling at the wrong places. Hopefully my disabling will work this time.

I noticed my mathlib fork also has been running these action since I-don't-know-when. (I see 12,896 workflow runs.) Is this necessary? Our PRs will appear and be checked in the upstream repo anyway. Isn't a waste of resource to run all these actions in forks?

[Bryan Gin-ge Chen]

Ching-Tsun Chou said:

I noticed my mathlib fork also has been running these action since I-don't-know-when. (I see 12,896 workflow runs.)

I just took a look at the actions in your fork: https://github.com/ctchou/mathlib4/actions . As far as I can tell they're all skipped, and don't actually run, which is as intended.

[Chris Henson]

I like some actions like linting running in forks so that I don't have to discover them on making a PR (and to turn it off it's a one time thing in the fork). Others like this should be configured as I describe above to not run in forks, and we can make that the default.

[Ching-Tsun Chou]

@Bryan Gin-ge Chen Thanks for checking. The status isn't clear from the top-level view. I thought they were all run.

[Ching-Tsun Chou]

@Chris Henson My preference is that even linting should be run in the upstream repo only. My habit is to push incomplete and often ill-conceived commits to a working branch in my fork all the time and later edit them using git rebase -i. I don't want all my random commits go through any checks. Lean itself already does plenty of checking.

[Chris Henson]

Ching-Tsun Chou said:

Chris Henson My preference is that even linting should be run in the upstream repo only.

That's fine, it is personal preference. For workflows that don't make sense outside the upstream repo, we can make it off by default. For anything where someone might reasonably want it in a fork, I think the status quo is fine. My reasoning is that it is easier to turn off the workflow in a fork via the UI (modulo GitHub navigation) than it is to have it off by default and turn it back on, which requires changing the YAML file.

[Chris Henson]

(If enough people feel differently that it should be off by default for all workflows, we can always make this chage later)

[Kim Morrison]

Chris Henson said:

We should probably add if: github.repository == 'leanprover/cslib' like other workflows so this doesn't happen for every fork

cslib#100

[Fabrizio Montesi]

merged, thanks :)

[Chris Henson]

@Fabrizio Montesi Can you merge cslib#102 as well? It's a related change Kim has approved.

[Fabrizio Montesi]

Yes, thanks for the heads up!