diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml new file mode 100644 index 0000000..1087424 --- /dev/null +++ b/.github/workflows/verify.yml @@ -0,0 +1,35 @@ +name: Verify contributions + +# Validates the whole solution/ graph before a change lands, on both events so +# that a direct push to main is covered as well as a pull request. +# +# Read-only, which is what makes it safe on a fork's branch. rebuild.yml is +# separate because pushing artifacts back needs write access, and an untrusted +# branch must not run with that. + +on: [push, pull_request] + +permissions: + contents: read + +concurrency: + # A pull request from a branch here raises both events; keying on its number + # puts them in one group so the duplicate is cancelled. + group: verify-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +defaults: + run: + shell: bash # for -o pipefail, so a failure piped through tee still fails + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-python@v7 + with: {python-version: '3.12'} + + - name: Verify the whole graph + run: python solution/validate_solution.py | tee -a "$GITHUB_STEP_SUMMARY" diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2fd81ec..c5c32a3 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -10,64 +10,72 @@ every Yellow reply or it does not. CI runs that check for you. Everything that defines the solution lives in `solution/`. Two files are hand-edited. -**`solution/steady_states.txt`** holds one block of six rows per diagram, top -row first, separated by blank lines: - -``` -....... -....... -.....|. -..=|.+. -2.=!1@- -2.21112 +**`solution/steady_states.json`** is a list of diagrams, each a list of six +rows, top row first: + +```json +[ + [ + " | ", + " ", + " | | ", + " =| + ", + "2 =!1@-", + "2 21112" + ] +] ``` - Exactly six rows of exactly seven characters. -- `!` urgent, `@` miai, `|` claimodd, `.` claimeven, `+` plus, `=` equal, +- `!` urgent, `@` miai, `|` claimodd, a space claimeven, `+` plus, `=` equal, `-` minus; `1` is a Red stone and `2` a Yellow stone. - The stones say which board a block belongs to, so it carries no separate identifier. - A `|` means different things on different rows. On an odd row it is a claimodd and can be played. On an even row it can never be played, and its - only effect is to stop that cell being a claimeven. `.` is the mirror of + only effect is to stop that cell being a claimeven. A space is the mirror of this, playable on an even row and silent on an odd one, so neither character is a blank. - A run of bars therefore marks the whole column as claimodd, each odd-row bar becoming playable as the column fills to that height, with the even-row bars between them suppressing the claimevens. Most such columns hold several claimodds rather than one. -- Write claimeven as `.`, not a space. A trailing space is invisible and gets - stripped by editors, which would silently shorten a row. +- A claimeven is a space, and the quoting keeps trailing ones intact, so count + the characters rather than trusting the eye: `"2 "` is a full row. - Only one of each mirror-equivalent pair is stored. The other orientation is re-derived when a representation is rendered, so do not add both. -**`solution/branches.txt`** holds one line per non-leaf Red-to-move node, -giving the single column Red commits to there: +**`solution/branches.json`** maps each non-leaf Red-to-move node to the single +column Red commits to there. The empty string is the empty board: -``` -41->5 -4153->5 +```json +{ + "": "4", + "41": "5", + "4153": "5" +} ``` -The two files interact. A node that gains a diagram stops being a -non-leaf node, so its line comes out of `branches.txt`. Anything that was only reachable -through it comes out too, both its branch lines and its diagrams. The validator -rejects entries it cannot reach, so a contribution that only adds is usually -incomplete. +The two files interact. A node that gains a diagram stops being a non-leaf +node, so its entry comes out of `branches.json`. Anything that was only +reachable through it comes out too, both its branches and its diagrams. The +validator rejects entries it cannot reach, so a contribution that only adds is +usually incomplete. It reports the frontier rather than the whole set, so +expect to run it, delete what it names, and run it again until it is quiet. A diagram contribution edits those two files and nothing else. Each subdirectory of `representations/` builds its artifacts from them with a -`render.py`, and CI rejects a pull request that edits `graph.js` or a `.pb`. -The webclient's 3D layout is a separate case: `spread_graph.py` nudges -`representations/webclient/positions.txt` rather than deriving it, so nothing -regenerates it automatically. +`render.py`, and those are rebuilt automatically after a change lands, so a +pull request should leave them alone. The webclient's 3D layout is a separate +case: `spread_graph.py` nudges `representations/webclient/positions.txt` +rather than deriving it, so nothing regenerates it automatically. ## What makes a diagram valid Red's move follows the priority list from the [explanation page](https://2swap.github.io/WeakC4/explanation/): win, block, -`!`, `@` (only when exactly one is playable), `|` on an odd row or `.` on an -even row, `+`, `=`, `-`. Red must win against *every* legal Yellow +`!`, `@` (only when exactly one is playable), `|` on an odd row or a space on +an even row, `+`, `=`, `-`. Red must win against *every* legal Yellow continuation; a draw is not enough. Two consequences of the site's guarantee that "there is always precisely one @@ -75,7 +83,9 @@ unique move suggested by this priority list": - **A tie between two markers at the same priority level is a failure**, not a coin flip. This has nothing to do with a drawn game. Two playable cells at - the applicable level means the diagram is rejected. Note that the viewer does + the applicable level means the diagram is rejected, with one exception: two + playable `@` do not tie, they cancel, and the next level decides instead. + Note that the viewer does not enforce this, since it only has to play a move and takes the leftmost of a tie, so watching the site play an ambiguous diagram will not reveal that it is ambiguous. Nothing there is checking. @@ -96,14 +106,16 @@ subtree below a move is its own certificate. ## Checking before you open a pull request -The checker needs only the standard library: +CI runs this on your pull request, but running it first is quicker than +waiting. It needs only the standard library: ```bash python solution/validate_solution.py ``` -It validates the whole solution in a few seconds. To see the shape of what you -have changed: +It validates the whole solution in a few seconds and prints a table of the +nine checks, with the failing entries listed underneath. To see the shape of +what you have changed: ```bash python solution/print_statistics.py @@ -111,10 +123,10 @@ python solution/print_statistics.py ## What CI does -Every push and pull request runs the same whole-solution check, and the result -appears in the **Summary** panel of the workflow run, linked from the Checks -tab. After a change lands on `main`, a second workflow re-renders whichever -representations depend on what changed and commits them. +Every push and pull request runs the whole-solution check, and the result +appears in the **Summary** panel of the run, linked from the Checks tab. After +a change lands on `main`, a second workflow re-renders the representations and +commits whatever changed, and a third publishes the site. A first-time contribution needs a maintainer to approve the run, so an empty Checks tab at first is normal. diff --git a/solution/validate_solution.py b/solution/validate_solution.py index 64fa39b..80b0da5 100644 --- a/solution/validate_solution.py +++ b/solution/validate_solution.py @@ -358,8 +358,10 @@ def check_yellow_children(branches, steady_states): continue child = [row[:] for row in board] child[y][x] = 2 + # Red's committed move lost the game, so nothing below matters. if makes_four(child, x, y, 2): - continue + raise AssertionError([position, rmove, ymove, + "Yellow wins the game with this reply"]) child_key = tuple(tuple(row) for row in child) canon = min(child_key, mirror_key(child_key)) @@ -416,6 +418,11 @@ def main(): help="parallel processes (default: one per core)") args = parser.parse_args() + # On Windows stdout falls back to the ANSI codepage whenever it is not a + # console (a pipe, a redirect, Git Bash), and cp1252 cannot encode the + # marks the table below is drawn with. + sys.stdout.reconfigure(encoding="utf-8") + jobs = args.jobs or (os.cpu_count() or 1) started = time.time()