chore: Only check the nightly tests on dafny-lang

[fabiomadge]

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[davidcok]

Don't do this -- there is no dependency of the doctests on the deep tests. It is useful to be able to check them even if Depp tests fail, even though they will have to wait until the deep tests pass to be merged.

[davidcok]

Please revert/don't merge these changes. This is adding dependencies in our CI, when we should be reducing them.

[fabiomadge]

This condition should now always pass when not running on dafny-lang/dafny. The rational for not running them is keeping nonessential load off CI while it's broken.

[davidcok]

Let me check my understanding. When pushes are made to a PR on a fork, do those resulting CI runs happen in a user's own account (and therefore will run anyway), despite a recent failure of the nightly tests?

[fabiomadge]

It depends on the target of the PR. If a PR is specified to merge into dafny-lang/dafny, it will run on the dafny-lang/dafny infrastructure, but if it will end up in the fork, the fork is footing the bill.

[keyboardDrummer]

Is there data to indicate we need to reduce load when the nightly is failing? It's costly to prevent other tests from running while nightly is broken since they block people from developing.

[fabiomadge]

What data are you looking for? This change doesn't block development in additional circumstances, but does unblocks us faster.

[keyboardDrummer]

What data are you looking for? This change doesn't block development in additional circumstances, but does unblocks us faster.

Doesn't this PR add additional deep-test checks for different workflows, for example here? There might be some confusion because this PR also changes the deep-test so it does not run on forks.

[fabiomadge]

Yes, in case a block is in place, it will apply to more tests, but it doesn't make the blocking more frequent. I don't think the marginal value of additional tests is constant. If they all run, then you're happy, as soon as a single required test is missing, you can't merge anyway. So there is limited value, while still consuming the scarce resources better used for fixing the broken tests.

[keyboardDrummer]

Yes, in case a block is in place, it will apply to more tests, but it doesn't make the blocking more frequent. I don't think the marginal value of additional tests is constant. If they all run, then you're happy, as soon as a single required test is missing, you can't merge anyway.

Shall we figure whether we should block (all) tests on the nightly failing or not, which this PR relates to? For that it's useful to know whether there is data to suggest not doing so causes a resource scarcity.

[fabiomadge]

I personally don't think gathering this data is worth the effort, but you can use your time how you see fit.

[keyboardDrummer]

I personally don't think gathering this data is worth the effort, but you can use your time how you see fit.

I was asking whether you have existing data that leads you to say the CI resources are too scarce to let us do regular builds while nightly is broken.

If we don't have that, why don't we try allowing the build to run when nightly is broken? If that turns out to cause a resource scarcity, we can disallow it again.

[fabiomadge]

I suspect we have different thresholds when it comes to accepting something as data. I did experience other builds delaying my CI fixes. Otherwise I wouldn't propose this change. I suspect this will only get worse with the new test schedule.

[keyboardDrummer]

I did experience other builds delaying my CI fixes. Otherwise I wouldn't propose this change.

Okay, I didn't realise that. I haven't noticed it, but maybe I didn't pay enough attention.

I'll leave it up to you and @davidcok to decide, but note that if we don't block the build we get to know better if it causes scarcity, and if we do block the build then we don't.