Repository navigation
feat: tie-breaking of optimal action values by random rewards [LWCGC24, Lemma 6] #10591
Workflow file for this run
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
| name: PR status | ||
|
Check warning on line 1 in .github/workflows/pr-status.yml
|
||
| # Keeps every PR's status label and its Zulip post current, reconciling in batches. | ||
| # | ||
| # This used to be three per-event workflows (pr-labels.yml's per-event jobs, zulip-pr.yml and | ||
| # zulip-pr-status.yml): one GitHub-hosted job for every label, comment, push and build event on every | ||
| # PR, over a thousand an hour, each spending most of its short life on setup. Those jobs competed with | ||
| # PR builds for the organisation's twenty GitHub-hosted slots. | ||
| # | ||
| # Now the events only wake this workflow. Its concurrency group is global, and GitHub admits one run | ||
| # at a time and keeps only the newest waiting run, cancelling the others before they take a runner. | ||
| # Each fresh scan reconciles every PR touched since its saved watermark | ||
| # (scripts/pr_status/batch.py), so an event whose own run was collapsed away is still covered by the | ||
| # run that replaced it. The price is latency: an update waits out a one-minute debounce (see the | ||
| # job's `environment`) and then the run ahead of it, typically one to three minutes in all. | ||
| # Failed runs retain unfinished work and quota deadlines in a verified artifact; | ||
| # the next run resumes without replaying its successful prefix. | ||
| # pr-labels.yml keeps the hourly reconcile-all sweep of labels and the manual re-sync. | ||
| on: | ||
| # Retry retained work even after the final PR event of a quiet period. | ||
| schedule: | ||
| - cron: "7 * * * *" | ||
| workflow_dispatch: | ||
| pull_request_target: | ||
| types: [opened, reopened, synchronize, closed, edited, converted_to_draft, ready_for_review, labeled, unlabeled] | ||
| workflow_run: | ||
| workflows: ["pr-build", "Review"] | ||
| types: [requested, completed] | ||
| issue_comment: | ||
| types: [created, edited, deleted] | ||
| permissions: | ||
| contents: read | ||
| actions: read | ||
| jobs: | ||
| app-credentials: | ||
| if: >- | ||
| ((github.repository == 'LeanMachineLearning/LMLExplore' && ( ((github.event_name == 'schedule' || github.event_name == 'workflow_dispatch') && github.ref == 'refs/heads/main') || (github.event_name == 'pull_request_target' && (github.event.action != 'edited' || github.event.changes.base != null)) || (github.event_name == 'workflow_run' && ((github.event.workflow_run.name == 'pr-build' && github.event.workflow_run.event == 'pull_request_target') || (github.event.workflow_run.name == 'Review' && github.event.action == 'completed'))) || (github.event_name == 'issue_comment' && github.event.issue.pull_request != null && (contains(github.event.comment.body, 'tauceti-scoreboard') || contains(github.event.changes.body.from, 'tauceti-scoreboard') )) ))) | ||
| runs-on: ubuntu-latest | ||
| permissions: {} | ||
| outputs: | ||
| ready: ${{ steps.check.outputs.ready }} | ||
| steps: | ||
| - name: Check App settings for setup | ||
| id: check | ||
| env: | ||
| APP_ID: ${{ secrets.APP_ID }} | ||
| APP_PRIVATE_KEY: ${{ secrets.APP_PRIVATE_KEY }} | ||
| shell: bash | ||
| run: | | ||
| ready=true | ||
| for name in APP_ID APP_PRIVATE_KEY; do | ||
| if [ -z "${!name}" ]; then | ||
| ready=false | ||
| printf 'Missing %s. Finish App credential setup with tauceti-tools doctor.\n' "$name" >> "$GITHUB_STEP_SUMMARY" | ||
| fi | ||
| done | ||
| printf 'ready=%s\n' "$ready" >> "$GITHUB_OUTPUT" | ||
| reconcile: | ||
| needs: app-credentials | ||
| # Meaningful PR events plus periodic/manual recovery; other events skip. | ||
| if: >- | ||
| needs.app-credentials.outputs.ready == 'true' && (github.repository == 'LeanMachineLearning/LMLExplore' && ( ((github.event_name == 'schedule' || github.event_name == 'workflow_dispatch') && github.ref == 'refs/heads/main') || (github.event_name == 'pull_request_target' && (github.event.action != 'edited' || github.event.changes.base != null)) || (github.event_name == 'workflow_run' && ((github.event.workflow_run.name == 'pr-build' && github.event.workflow_run.event == 'pull_request_target') || (github.event.workflow_run.name == 'Review' && github.event.action == 'completed'))) || (github.event_name == 'issue_comment' && github.event.issue.pull_request != null && (contains(github.event.comment.body, 'tauceti-scoreboard') || contains(github.event.changes.body.from, 'tauceti-scoreboard') )) )) | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 30 | ||
| # On the job, not the workflow: a workflow-level group admits runs before the `if` above is | ||
| # evaluated, so an irrelevant event could displace the one pending run that mattered and then | ||
| # skip. Here only runs that pass the filter enter the group. (Nothing else may share it: GitHub | ||
| # replaces a pending member with the newest, so a different kind of job would cancel a batch.) | ||
| concurrency: | ||
| group: pr-status | ||
| cancel-in-progress: false | ||
| # A one-minute debounce that holds no runner. The pr-status-debounce environment's only | ||
| # protection rule is a one-minute wait timer; a job waiting on it holds the concurrency group | ||
| # but no runner, while newer events collapse into the one pending run behind it. Without it, | ||
| # events arriving continuously kept one runner busy back to back; with it, a batch runs at most | ||
| # about every two minutes (the wait plus the batch) and covers everything that arrived meanwhile. | ||
| # `deployment: false` keeps the wait timer without recording a deployment for every batch. | ||
| # Keep secrets out of this environment: they would become available to the job. | ||
| environment: | ||
| name: pr-status-debounce | ||
| deployment: false | ||
| steps: | ||
| - uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1; v1 ignores permission-* inputs | ||
| id: app-token | ||
| with: | ||
| app-id: ${{ secrets.APP_ID }} | ||
| private-key: ${{ secrets.APP_PRIVATE_KEY }} | ||
| owner: LeanMachineLearning | ||
| repositories: LMLExplore | ||
| permission-issues: write | ||
| permission-pull-requests: write | ||
| permission-contents: read | ||
| # No `actions` permission: the App does not hold it, and the run listings batch.py reads | ||
| # are public for this public repository. | ||
| # The trusted base checkout: the scripts that run are the ones on the target branch, never the | ||
| # version proposed by the PR. | ||
| - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 | ||
| with: | ||
| # The policy checkout below is a local action, so it must come from this trusted checkout. | ||
| sparse-checkout: | | ||
| scripts/pr_status | ||
| .github/actions/checkout-merge-policy | ||
| persist-credentials: false | ||
| - name: Prepare pinned shared tools | ||
| uses: TauCetiProject/TauCetiTools/.github/actions/setup@68ca7893e90b82454ab58ba64dca753a05cd2720 | ||
| with: | ||
| tools-repository: TauCetiProject/TauCetiTools | ||
| tools-ref: 68ca7893e90b82454ab58ba64dca753a05cd2720 | ||
| project-directory: . | ||
| - name: Checkout the pinned merge policy (read-only) | ||
| uses: ./.github/actions/checkout-merge-policy | ||
| # Discover artifacts directly: cancelled pending runs have no artifact and | ||
| # can otherwise crowd the last useful checkpoint out of a run listing. | ||
| - name: Restore latest trusted progress | ||
| env: | ||
| GH_TOKEN: ${{ github.token }} | ||
| REPO: ${{ github.repository }} | ||
| run: | | ||
| set -euo pipefail | ||
| mkdir -p "$RUNNER_TEMP/state-in" | ||
| trusted_run=$(cat scripts/pr_status/trusted-run.jq) | ||
| ids=$(gh api "repos/$REPO/actions/artifacts?name=pr-status-progress&per_page=10" \ | ||
| --jq '.artifacts | sort_by(.created_at) | reverse | .[] | select(.expired == false) | .workflow_run.id') | ||
| for id in $ids; do | ||
| trusted=$(gh api "repos/$REPO/actions/runs/$id" --jq "$trusted_run") | ||
| if [ "$trusted" = true ]; then | ||
| gh run download "$id" -R "$REPO" -n pr-status-progress -D "$RUNNER_TEMP/state-in" | ||
| break | ||
| fi | ||
| done | ||
| # Cold-start --since fallback only; restored progress owns its watermark. | ||
| # Use the last trusted success, overlapping two minutes and capped at 48h; | ||
| # before any success, inspect the previous two hours. A lookup failure fails | ||
| # the job rather than guessing. | ||
| - name: Find where the previous run started | ||
| id: since | ||
| env: | ||
| GH_TOKEN: ${{ github.token }} | ||
| run: | | ||
| set -euo pipefail | ||
| trusted_run=$(cat scripts/pr_status/trusted-run.jq) | ||
| prev=$(gh api "repos/${{ github.repository }}/actions/workflows/pr-status.yml/runs?status=success&per_page=10" \ | ||
| --jq "[.workflow_runs[] | select($trusted_run)] | .[0]") | ||
| last=$(jq -r '.run_started_at // ""' <<< "$prev") | ||
| id=$(jq -r '.id // ""' <<< "$prev") | ||
| # One-time migration of the former retry-only artifact when no new | ||
| # checkpoint exists. Missing legacy state uses the cold-start window. | ||
| if [ ! -f "$RUNNER_TEMP/state-in/state.json" ] && [ -n "$id" ]; then | ||
| gh run download "$id" -R "${{ github.repository }}" -n pr-status-retry -D "$RUNNER_TEMP/state-in" \ | ||
| 2>/dev/null || true | ||
| fi | ||
| if [ -f "$RUNNER_TEMP/state-in/retry.json" ]; then | ||
| mv "$RUNNER_TEMP/state-in/retry.json" "$RUNNER_TEMP/state-in/state.json" | ||
| fi | ||
| python3 - "$last" >> "$GITHUB_OUTPUT" <<'EOF' | ||
| import datetime as dt, sys | ||
| now = dt.datetime.now(dt.timezone.utc) | ||
| if sys.argv[1]: | ||
| t = dt.datetime.fromisoformat(sys.argv[1].replace("Z", "+00:00")) - dt.timedelta(minutes=2) | ||
| else: | ||
| t = now - dt.timedelta(hours=2) | ||
| t = max(t, now - dt.timedelta(hours=48)) | ||
| print("since=" + t.strftime("%Y-%m-%dT%H:%M:%SZ")) | ||
| EOF | ||
| - name: Reconcile PR status labels | ||
| env: | ||
| GH_TOKEN: ${{ steps.app-token.outputs.token }} | ||
| GH_REPO: ${{ github.repository }} | ||
| ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} | ||
| ZULIP_EMAIL: ${{ secrets.ZULIP_EMAIL }} | ||
| ZULIP_SITE: | ||
| SINCE: ${{ steps.since.outputs.since }} | ||
| # The event's own PR, when its payload names one, goes first. | ||
| PR: ${{ github.event.pull_request.number || github.event.issue.number || github.event.workflow_run.pull_requests[0].number }} | ||
| # From the repository root: readiness finds the pinned policy at .tauceti-review/runner. | ||
| run: | | ||
| args=(--labels-only --since "$SINCE" --state-in "$RUNNER_TEMP/state-in/state.json" --state-out "$RUNNER_TEMP/progress/state.json") | ||
| mkdir -p "$RUNNER_TEMP/progress" | ||
| case "$PR" in ''|*[!0-9]*) ;; *) args+=(--pr "$PR") ;; esac | ||
| python3 scripts/pr_status/batch.py "${args[@]}" | ||
| - name: Save completed progress and unfinished work | ||
| if: always() | ||
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | ||
| with: | ||
| name: pr-status-progress | ||
| path: ${{ runner.temp }}/progress/state.json | ||
| if-no-files-found: error | ||
| retention-days: 7 | ||
| overwrite: true | ||
