tlaplus
Protect master branch
Several commits (for example, the latest one 9ece37b2e6d5cab0de16582ea81733ce5f586a84) have broken the CI because they were committed directly to master. I propose making master a protected branch so commits must pass the CI first.
@muenchnerkindl @lemmy could this please be implemented? It should be a simple checkmark somewhere in the repository settings.
Our CI pipeline is overly complex and brittle, which is why commits are failing. That is the root cause we need to address—not the symptoms. The commit you referenced is a good example: there is nothing wrong with it at the TLA+ level. It failed solely due to metadata checks that should not be enforced.
Committing directly to master branch, breaking the CI, then making no attempt to fix it or raise it as an issue is considered unacceptable behavior in every development environment I can imagine. That is what should be addressed. If you open a PR and the checks are failing for reasons you think are bad, fine - I can help you fix it! Just pushing those commits to master and breaking the CI for everybody is not a good thing to do.
I will not continue this discussion. I’ve consistently argued that the new CI system is complex and prone to failure (check your inbox and other issues). Despite this, you proceeded with it and now expect others to address the resulting CI failures on their time.
Commit 9ece37b2e6d5cab0de16582ea81733ce5f586a84 fixes a subtle but critical issue that broke TLC model checking. This fix is orders of magnitude more important than the CI metadata checks in the TLA+ example repository. The TLA+ examples themselves are correct; the problem lies solely in the CI machinery.
The TLA+ examples are correct (and we know them to be so) because of the CI machinery. I have put in a bunch of work in #171 to make the CI more robust and contribution process easier, following directly from your feedback. Reciprocity is what makes open source go around.
I see my feedback itself as a form of reciprocity. Also, to clarify, I didn’t know my TLA+ changes were correct because of the CI — I verified them manually before pushing.
This actually highlights another issue with the CI metadata checks: it’s not easy to check locally whether the metadata checks will fail. Doing so requires installing and running an additional tool, which I (and likely others) am not willing to do. As a result, CI ends up being the first place where these problems surface.
Excepting Python, all tools are downloaded & extracted under the root repo directory and do not pollute the system package store. Directions on running them locally are documented here: https://github.com/tlaplus/Examples/blob/master/DEVELOPING.md#running-the-scripts
I appreciate the intention to check commits as thoroughly as possible, but my experience with getting https://github.com/tlaplus/Examples/pull/190 through the CI indicates that I do not have the competence required to appreciate CI failures, or even to check that successful CI runs indeed provide evidence that the right checks were made.
The question of performing the checks locally is moot for the problems that I encountered because they were related to timing issues on the GitHub runners.
