Disable typecheck, link-check, and pre-commit workflows on master#1552
Merged
VojtechStep merged 7 commits intoUniMath:masterfrom Sep 25, 2025
Merged
Disable typecheck, link-check, and pre-commit workflows on master#1552VojtechStep merged 7 commits intoUniMath:masterfrom
typecheck, link-check, and pre-commit workflows on master#1552VojtechStep merged 7 commits intoUniMath:masterfrom
Conversation
Collaborator
|
Since we require PRs to be up-to-date before merging them, does it even make sense to run precommit and link-check on master? We could have incremental typechecking and style checking in PRs, and then master does a clean build (which typechecks) and deployment (which linkchecks). WDYT? |
Collaborator
Author
|
Yeah that sounds good! In the past I was thinking of these redundancies as double checks that the workflows were working properly, but in the current state of affairs I agree we can do without them. The problems don't have to be detected on master anyways; if we find an issue later, we've found the issue. |
fredrik-bakke
changed the title
typecheck workflow on mastertypecheck, link-check, and pre-commit workflows on master
Collaborator
Author
|
@VojtechStep updated now |
Collaborator
|
LGTM! (for some reason GitHub decided to delay the ping notification for two hours) |
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
Oct 17, 2025
…er (UniMath#1552) The previous change to the `typecheck` workflow UniMath#1493 contained a mistake that made it skip on commits to the master branch, which was unintended. However, I believe that we in fact do not need to run it on master, since it is already tested in the pull request branch, and besides, the benchmarking workflow also verifies that master type checks. Hence, this PR hides the workflow from the workflow agenda on master. It does so by creating a new ci file. This PR also renames the benchmarking/profiling workflow to "Clean build and profiling of library". I've still added an inclusion rule so that if we in the future wish to run it on commits to a certain branch we only need to add an "on push" entry and not edit the if clause for `typecheck`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The previous change to the
typecheckworkflow #1493 contained a mistake that made it skip on commits to the master branch, which was unintended. However, I believe that we in fact do not need to run it on master, since it is already tested in the pull request branch, and besides, the benchmarking workflow also verifies that master type checks. Hence, this PR hides the workflow from the workflow agenda on master. It does so by creating a new ci file.This PR also renames the benchmarking/profiling workflow to "Clean build and profiling of library".
I've still added an inclusion rule so that if we in the future wish to run it on commits to a certain branch we only need to add an "on push" entry and not edit the if clause for
typecheck.