feat: let anyone publish a progress report

.github/scripts/collect.py

@@ -26,11 +26,12 @@
 * The previous contents of the two files are read at `main_sha`, not from a working checkout that
   could have drifted.
 
-Run as: collect.py --repo O/R --pr N --allowed-user-ids 1,2 --out bundle.json
+Run as: collect.py --repo O/R --pr N --out bundle.json
 """
 
 import argparse
 import base64
+import datetime
 import json
 import pathlib
 import re
@@ -41,6 +42,12 @@
 
 from progress import files, gate  # noqa: E402
 
+# Where the reported window has to live. `to_sha` is checked for reachability from this branch, which
+# tracks the newest TauCeti commit with published documentation.
+CODE_REPO = "TauCetiProject/TauCeti"
+CODE_REF = "docgen"
+ROADMAP_LABEL_PREFIX = "roadmap/"
+
 # `compare` returns at most 300 files. More than that cannot be a progress report, and a truncated
 # list could HIDE a path from the gate, so anything approaching the limit is refused outright rather
 # than partially inspected.
@@ -150,11 +157,103 @@ def file_at(repo, ref, path):
     return content
 
 
+def last_commit_date(repo, ref, path):
+    """When `path` was last changed on `ref`, or None if never.
+
+    Used to enforce the per-roadmap reporting cadence on the server. Read from the base branch, so it
+    reflects reports that actually landed rather than anything the pull request claims.
+    """
+    proc = subprocess.run(
+        ["gh", "api", f"repos/{repo}/commits?sha={ref}&path={path}&per_page=1",
+         "--jq", ".[0].commit.committer.date"],
+        capture_output=True, text=True,
+    )
+    if proc.returncode != 0:
+        raise CollectError(f"reading the history of {path} failed: {proc.stderr.strip()}")
+    out = proc.stdout.strip()
+    return out if out and out != "null" else None
+
+
+def rev_parse(repo, ref):
+    """Resolve a ref to an immutable commit SHA, or None if it cannot be read."""
+    proc = subprocess.run(
+        ["gh", "api", f"repos/{repo}/commits/{ref}", "--jq", ".sha"],
+        capture_output=True, text=True,
+    )
+    return proc.stdout.strip() or None if proc.returncode == 0 else None
+
+
+def compare_status(repo, base, head):
+    """`status` from a two-dot-three comparison, or None when either end is not a commit.
+
+    A 404 here is a *finding*, not an error: it is exactly what a fabricated `to_sha` looks like, and
+    the caller turns it into a refusal.
+    """
+    proc = subprocess.run(
+        ["gh", "api", f"repos/{repo}/compare/{base}...{head}", "--jq", ".status"],
+        capture_output=True, text=True,
+    )
+    if proc.returncode != 0:
+        err = proc.stderr or ""
+        if "Not Found" in err or "404" in err:
+            return None
+        raise CollectError(f"comparing {base[:7]}...{head[:7]} in {repo} failed: {err.strip()}")
+    return proc.stdout.strip() or None
+
+
+def resolve_window(new_progress, repo=CODE_REPO, ref=CODE_REF):
+    """Check the newly-appended section's window against real TauCeti history.
+
+    Without this, `to_sha` is unconstrained. Cursor continuity pins `from_sha` to the area's current
+    cursor, but nothing stopped a report naming an arbitrary 40-hex `to_sha`, landing, and leaving the
+    cursor there -- then repeating from that value indefinitely, walking the cursor past windows that
+    could never afterwards be reported and announcing every step to Zulip.
+
+    Two questions, both answered against `ref`:
+
+    * is `to_sha` a commit reachable from the documentation branch?
+    * does it come strictly after `from_sha`?
+
+    Reachability rather than equality with the tip, because the tip advances whenever documentation is
+    published and equality would refuse a report that was correct when its round began.
+
+    Returns None when the section cannot be parsed; the content checks report that failure properly.
+    """
+    try:
+        sections = files.parse_sections(new_progress or "")
+    except files.FormatError:
+        return None
+    if not sections:
+        return None
+    section = sections[-1]
+    from_sha, to_sha = section["from_sha"], section["to_sha"]
+
+    # `to_sha...ref` is `ahead` when ref has commits to_sha does not, and `identical` when to_sha IS
+    # the tip. Both mean to_sha is reachable. `behind` or `diverged` mean it is off the branch.
+    # Resolve the branch to an immutable SHA first and compare against that. `docgen` is a mutable
+    # ref: comparing against the name leaves a gap in which it could move between the question and
+    # the answer, and records nothing about what was actually consulted.
+    tip = rev_parse(repo, ref)
+    if tip is None:
+        return {"repo": repo, "ref": ref, "ref_sha": None, "from_sha": from_sha, "to_sha": to_sha,
+                "to_reachable": False, "advances": None}
+    reach = compare_status(repo, to_sha, tip)
+    to_reachable = reach in ("ahead", "identical")
+
+    advances = None
+    if to_reachable:
+        # Only `ahead` advances: `identical` is an empty window, and `behind`/`diverged` go backwards
+        # or sideways.
+        advances = compare_status(repo, from_sha, to_sha) == "ahead"
+
+    return {"repo": repo, "ref": ref, "ref_sha": tip, "from_sha": from_sha, "to_sha": to_sha,
+            "to_reachable": to_reachable, "advances": advances}
+
+
 def main(argv=None):
     ap = argparse.ArgumentParser()
     ap.add_argument("--repo", required=True)
     ap.add_argument("--pr", required=True, type=int)
-    ap.add_argument("--allowed-user-ids", required=True)
     ap.add_argument("--base-branch", default="main")
     ap.add_argument("--out", required=True)
     args = ap.parse_args(argv)
@@ -168,6 +267,7 @@ def main(argv=None):
     if not main_sha:
         raise CollectError(f"could not resolve {args.base_branch}")
 
+
     # The area comes from the branch and is validated by the gate's own pattern. Reading it here with
     # the gate's regex keeps the two from disagreeing.
     branch = (pr.get("head") or {}).get("ref") or ""
@@ -216,7 +316,8 @@ def blob_for(basename):
     # `TauCetiRoadmap/` first was a real hole: an area can exist under both parents, so a pull request
     # changing `Completed/<area>/` would be handed the ACTIVE log as its append-only baseline, and a
     # wholesale replacement of the archived log then looked like a valid append.
-    old_status = old_progress = None
+    old_status = old_progress = last_report_at = None
+    area_exists = False
     old_paths = {}
     current_cursor = None
     parents = {gate.PATH_RE.match(p).group(1) for p in by_path}
@@ -231,6 +332,12 @@ def blob_for(basename):
         }
         old_status = file_at(args.repo, main_sha, old_paths["STATUS.md"])
         old_progress = file_at(args.repo, main_sha, old_paths["PROGRESS.md"])
+        # When this roadmap was last reported, for the server-side cadence limit.
+        last_report_at = last_commit_date(args.repo, main_sha, old_paths["PROGRESS.md"])
+        # A roadmap is a directory with a README.md, the same rule the planner uses. Reports may only
+        # be added to one that already exists, or invented area names would give unlimited
+        # "first reports", each exempt from the cadence limit.
+        area_exists = file_at(args.repo, main_sha, f"{parent}/{area}/README.md") is not None
         if old_progress:
             try:
                 current_cursor = files.cursor(old_progress)
@@ -256,7 +363,11 @@ def blob_for(basename):
 
     bundle = {
         "base_repo": args.repo,
-        "allowed_user_ids": [int(x) for x in re.split(r"[,\s]+", args.allowed_user_ids) if x],
+        "code_window": resolve_window(new_progress),
+        "area_exists": area_exists,
+        "last_report_at": last_report_at,
+        # The collector's own clock, never anything from the pull request.
+        "collected_at": datetime.datetime.now(datetime.timezone.utc).isoformat(),
         "pr": pr,
         "area": area,
         "head_sha": head_sha,

.github/workflows/merge.yml

@@ -37,10 +37,6 @@ on:
         description: The TauCetiProgress ref to validate with (must equal the `uses:` SHA).
         required: true
         type: string
-      allowed_user_ids:
-        description: Comma-separated numeric GitHub user ids permitted to author these PRs.
-        required: true
-        type: string
       app_id:
         description: >
           Numeric id of the App whose token performs the merge. It MUST be an App that the target
@@ -59,19 +55,39 @@ on:
       APP_PRIVATE_KEY:
         required: true
 
+# The floor for both jobs. `validate` raises its own to write, for one comment; `merge` does not
+# need it at all, because everything it writes uses the App token rather than this one.
 permissions:
   contents: read
   pull-requests: read
 
-# Repository-wide, not per-PR: two progress PRs must never be validated and merged concurrently,
-# because each one's validity depends on where `main` currently is.
-concurrency:
-  group: progress-merge
-  cancel-in-progress: false
+# DELIBERATELY NOT SERIALISED.
+#
+# An earlier version put every call into one repository-wide `progress-merge` concurrency group, so
+# that two reports could never be validated and merged at once, each one's validity depending on
+# where `main` is. That reasoning was right about the hazard and wrong about the remedy. GitHub keeps
+# one running and one pending run per group and discards the older pending one when a newer event
+# arrives, so with anyone able to open and synchronise a `progress/*` pull request, the group becomes
+# a lever: a steady trickle of events evicts the queued legitimate run indefinitely, and nothing
+# reports an error.
+#
+# Concurrent runs are safe without it. The landing step is a compare-and-swap: the commit names the
+# validated `main` SHA as its only parent and the ref update sets `force=false`, so if another report
+# landed in between, this one's update is not a fast-forward and is rejected. The loser fails its
+# swap and the pull request is simply rebuilt on the newer `main` next round -- which is exactly what
+# the serialisation was there to prevent, achieved by the mechanism that was already doing the work.
 
 jobs:
   validate:
     runs-on: ubuntu-latest
+    # `write` ONLY here, and only so a refusal can be explained on the pull request itself. Anyone
+    # may publish a report now, so a contributor whose report is refused would otherwise get no
+    # feedback at all: the reason would sit in the Actions log of a workflow in a repository they may
+    # not be able to read. This job never checks out or executes pull-request content, and the
+    # comment body is written to a file rather than interpolated into a shell.
+    permissions:
+      contents: read
+      pull-requests: write
     outputs:
       verdict: ${{ steps.gate.outputs.verdict }}
       head_sha: ${{ steps.gate.outputs.head_sha }}
@@ -97,11 +113,10 @@ jobs:
           GH_TOKEN: ${{ github.token }}
           PR: ${{ inputs.pr }}
           REPO: ${{ github.repository }}
-          ALLOWED: ${{ inputs.allowed_user_ids }}
         run: |
           set -euo pipefail
           python3 validator/.github/scripts/collect.py \
-            --repo "$REPO" --pr "$PR" --allowed-user-ids "$ALLOWED" --out bundle.json
+            --repo "$REPO" --pr "$PR" --out bundle.json
 
       # The gate. Exit 0 allows, exit 3 is a considered refusal, anything else is a crash. A crash
       # must NOT read as a refusal: the two are different, and conflating them turns an unexpected
@@ -154,6 +169,10 @@ jobs:
           } > refusal.md
           printf 'gate refused:\n'
           cat refusal.md
+          # Best effort. A refusal is a normal outcome, so failing to describe it must not turn the
+          # run red -- the verdict is already recorded in the job output either way.
+          gh pr comment "$PR" --repo "$REPO" --body-file refusal.md \
+            || echo "::warning title=refusal not posted::could not comment on #$PR" 
 
   merge:
     needs: validate
@@ -286,4 +305,15 @@ jobs:
           # Best effort from here: neither of these affects correctness.
           gh pr comment "$PR" --repo "$REPO" \
             --body "Landed on \`main\` as $COMMIT by compare-and-swap on the validated tree." || true
-          gh api -X DELETE "repos/$REPO/git/refs/heads/$(gh pr view "$PR" --repo "$REPO" --json headRefName --jq .headRefName)" > /dev/null 2>&1 || true
+          # Delete the source branch ONLY when it is in this repository. Branch names are a pure
+          # function of the window, so a fork's branch has the same name as the canonical one would:
+          # deleting `repos/$REPO/git/refs/heads/<name>` after landing a FORK pull request would
+          # delete an unrelated canonical branch that happens to share the name.
+          head_repo="$(gh pr view "$PR" --repo "$REPO" --json headRepository,headRepositoryOwner \
+                       --jq '(.headRepositoryOwner.login // "") + "/" + (.headRepository.name // "")')"
+          head_ref="$(gh pr view "$PR" --repo "$REPO" --json headRefName --jq .headRefName)"
+          if [ "$head_repo" = "$REPO" ] && [ -n "$head_ref" ]; then
+            gh api -X DELETE "repos/$REPO/git/refs/heads/$head_ref" > /dev/null 2>&1 || true
+          else
+            echo "head is in $head_repo, not $REPO; leaving its branch alone"
+          fi

build/lib/progress/announce.py

@@ -0,0 +1,119 @@
+"""Announce a new PROGRESS.md section in Zulip, idempotently.
+
+Idempotency is the whole design here, because the alternatives are both bad: post before the merge
+and a failed merge announces work that never landed; post after the merge with no dedup and a
+re-run of the workflow (or a retry after a lost response) posts the section twice.
+
+So each section carries a stable id derived from its window, the id is embedded in the message, and
+posting searches the topic for that id first. Re-running is then free, and a genuine transient
+failure can be retried by re-running the workflow.
+
+This runs in CI, not on the worker: the Zulip credentials are GitHub secrets, and the worker holds
+none. It is also a separate job from the merge, so the App token that can write to the roadmap repo
+and the Zulip key never sit in the same job.
+"""
+
+import pathlib
+import re
+
+from . import files, zulip
+
+# The visible marker that makes a post findable. Zulip has no hidden metadata, and an HTML comment
+# does not survive rendering, so the id is a short visible tag at the end of the message.
+ID_PREFIX = "progress-log-id:"
+
+MAX_MESSAGE_CHARS = 8000
+
+
+def section_id(header):
+    """A stable id for a window: `<Area>-<from7>-<to7>`."""
+    return f"{header['roadmap']}-{header['from_sha'][:7]}-{header['to_sha'][:7]}"
+
+
+def split_section(text):
+    """`(header, prose)` for the appended text of a `PROGRESS.md` update.
+
+    Note what `text` actually is: everything the update added to the file. For an area's *first*
+    report that includes the file preamble ahead of the section, not just the section, so this cannot
+    assume the text begins at the marker. It takes the prose after the last section marker's heading,
+    which is right in both cases.
+    """
+    headers = files.parse_sections(text)
+    if len(headers) != 1:
+        raise files.FormatError(f"expected exactly one section, found {len(headers)}")
+    m = re.search(r"<!--tauceti-progress:v1 .*?-->[^\n]*\n", text, flags=re.S)
+    if not m:
+        raise files.FormatError("no section marker found in the appended text")
+    body = text[m.end():]
+    # Drop the `## ...` heading too; Zulip gets a lead-in of our own.
+    body = re.sub(r"\A\s*##[^\n]*\n", "", body).strip()
+    return headers[0], body
+
+
+def render_message(header, prose, roadmap_url=None):
+    """The Zulip message for one section.
+
+    Shape follows the review Kim gave Chris's bot: `TauCeti#NNN` linkifiers rather than markdown
+    links, no claims about what Mathlib does or does not have, and no hidden trailing tag (Zulip
+    renders none, so the id is visible).
+    """
+    area = header["roadmap"]
+    prs = header["prs"]
+    body = zulip.sanitize(prose)
+    if len(body) > MAX_MESSAGE_CHARS:
+        body = body[:MAX_MESSAGE_CHARS].rsplit("\n", 1)[0] + "\n\n(truncated; the full section is in `PROGRESS.md`)"
+    link = roadmap_url or (
+        f"https://github.com/TauCetiProject/TauCetiRoadmap/blob/main/"
+        f"TauCetiRoadmap/{area}/PROGRESS.md"
+    )
+    return (
+        f"**{area}** — progress on {len(prs)} merged pull requests "
+        f"(`{header['from_sha'][:7]}` to `{header['to_sha'][:7]}`)\n\n"
+        f"{body}\n\n"
+        f"Full log: {link}\n"
+        f"{ID_PREFIX}{section_id(header)}"
+    )
+
+
+def already_posted(client, channel, topic, sid):
+    """Has this section already been announced?
+
+    Searches for the id and then confirms the id actually appears in the message text, because
+    Zulip's search is word-based and can return near matches.
+    """
+    needle = f"{ID_PREFIX}{sid}"
+    for msg in client.search(channel, topic, sid):
+        if needle in (msg.get("content") or ""):
+            return msg
+    return None
+
+
+def run(section_file, channel=None, topic=None, dry_run=False):
+    """Post the section in `section_file`. Returns a process exit code.
+
+    Raises on a transient failure rather than swallowing it, so the workflow run goes red and a
+    retry is meaningful. The dedup check above is what makes that retry safe.
+    """
+    channel = channel or zulip.DEFAULT_CHANNEL
+    topic = topic or zulip.DEFAULT_TOPIC
+
+    text = pathlib.Path(section_file).read_text(encoding="utf-8")
+    header, prose = split_section(text)
+    sid = section_id(header)
+    message = render_message(header, prose)
+
+    if dry_run:
+        print(f"[dry-run] would post to {channel} > {topic} as {sid}:\n\n{message}")
+        return 0
+
+    client = zulip.from_env()
+    client.check(channel)
+
+    existing = already_posted(client, channel, topic, sid)
+    if existing is not None:
+        print(f"already announced as message {existing['id']}; nothing to do")
+        return 0
+
+    mid = client.send(channel, topic, message)
+    print(f"posted message {mid} for {sid}")
+    return 0