Repository navigation
Reduce Erdos97ConvexOctagon peak compiler memory #3341
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: Proof Profile | |
| # Keep a sticky profile comment on every PR, including drafts, and refresh it | |
| # after pushes or reopening. The PR author or anyone with write access can | |
| # also comment `/profile`; workflow_dispatch takes an explicit PR number. | |
| # | |
| # Added files get an absolute profile (`lean --profile` + heartbeat counts). | |
| # Modified files instead get a base→head compile-cost comparison: heartbeats | |
| # and wall time are measured for the base and head sources, and the comment | |
| # reports the deltas. That answers the right question for refactor PRs — | |
| # "did this golf change compile cost?" — where absolute numbers alone are | |
| # noise. On PRs that change the toolchain/manifest (or when no warm build | |
| # cache exists) the comparison is skipped and modified files fall back to | |
| # the absolute profile. | |
| # | |
| # Modified files also get a textual statement-change report (statements.py, | |
| # the same parser physlib's /check-golf uses): how many declarations — and | |
| # which — changed their *statement* rather than only their proof/body. This | |
| # needs no build, so it renders even when the compile-cost comparison is | |
| # skipped; it is the reassurance a refactor wants that no theorem was quietly | |
| # restated. | |
| # | |
| # Speed (same approach as physlib's /check-golf): measurement only needs the | |
| # measured files' *imports* built, never the whole library, so `lake build` | |
| # targets just the changed modules. Both sides of a comparison are elaborated | |
| # against the single merge-base environment (whose build is ~all cache hits) — | |
| # sound when only proofs/bodies change, which is what a refactor PR does; a | |
| # head file that no longer compiles there is flagged in the comment. Sources | |
| # come from `git show`, so no checkout juggling. (Measurement logs are not | |
| # cached across runs: the cache service denies writes to comment-triggered | |
| # runs outright, and with the two sides in parallel jobs a cached base pass | |
| # would not shorten the wall clock anyway.) | |
| # | |
| # Structure: a cheap `plan` job resolves the PR and decides what to measure; | |
| # the comparison then fans out as parallel `measure` matrix jobs — each side | |
| # (base/head) is split at run time into up to 8 round-robin shards of the | |
| # modified-file list, so the wall clock is one shard's worth of measurement | |
| # plus setup, and there is no static shard assignment to maintain as the | |
| # pool grows; `absolute` profiles any added files; `report` stitches the | |
| # shard logs back together and stages the PR comment for the posting | |
| # companion workflow. The measurement and render scripts are fetched from | |
| # scripts/proof-profile/ on the default branch — not from the PR checkout — | |
| # so they stay in lockstep with this workflow file (which issue_comment runs | |
| # also take from the default branch). | |
| on: | |
| pull_request: | |
| types: [opened, synchronize, reopened, ready_for_review] | |
| issue_comment: | |
| types: [created] | |
| workflow_dispatch: | |
| inputs: | |
| pr_number: | |
| description: "PR number to profile" | |
| required: true | |
| type: string | |
| permissions: | |
| contents: read | |
| # These jobs run the PR's Lean code, so they stay least-privilege: they | |
| # read PR metadata but never post (the `Proof Profile Comment` workflow | |
| # does). | |
| pull-requests: read | |
| # Workflow-level concurrency applies to every run regardless of the job-level | |
| # `if:`, so an `issue_comment` event for a non-`/profile` comment (e.g. `/review`) | |
| # would otherwise enter `proof-profile-<pr>` and cancel an in-flight `/profile` | |
| # run before the body check could short-circuit it. Route non-matching events | |
| # into a unique per-run group so they can't steal the slot. | |
| concurrency: | |
| group: >- | |
| ${{ | |
| (github.event_name == 'workflow_dispatch' || | |
| github.event_name == 'pull_request' || | |
| (github.event_name == 'issue_comment' && | |
| startsWith(github.event.comment.body, '/profile'))) | |
| && format('proof-profile-{0}', | |
| github.event.pull_request.number || | |
| github.event.issue.number || | |
| inputs.pr_number) | |
| || format('proof-profile-noop-{0}', github.run_id) | |
| }} | |
| cancel-in-progress: true | |
| jobs: | |
| plan: | |
| runs-on: ubuntu-latest | |
| name: Plan profile | |
| # Automatic PR events also support drafts. For issue comments, run only | |
| # when the body starts with `/profile` AND the commenter is | |
| # either the PR author or someone with write access. The measurement jobs | |
| # check out and *run* the PR's Lean code, so the workflow stays | |
| # least-privilege (read-only token, no secrets) and the workflow | |
| # definition always comes from the base default branch (issue_comment | |
| # context), while barring an arbitrary commenter from triggering a run | |
| # on someone else's fork PR. | |
| if: >- | |
| github.event_name == 'workflow_dispatch' || | |
| github.event_name == 'pull_request' || | |
| (github.event_name == 'issue_comment' && | |
| github.event.issue.pull_request != null && | |
| startsWith(github.event.comment.body, '/profile') && | |
| (github.event.comment.user.login == github.event.issue.user.login || | |
| contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association))) | |
| outputs: | |
| number: ${{ steps.pr.outputs.number }} | |
| head_sha: ${{ steps.pr.outputs.head_sha }} | |
| base_sha: ${{ steps.pr.outputs.base_sha }} | |
| files: ${{ steps.files.outputs.files }} | |
| added: ${{ steps.files.outputs.added }} | |
| modified: ${{ steps.files.outputs.modified }} | |
| profile_files: ${{ steps.files.outputs.profile_files }} | |
| compare: ${{ steps.files.outputs.compare }} | |
| compare_note: ${{ steps.files.outputs.compare_note }} | |
| merge_base: ${{ steps.files.outputs.merge_base }} | |
| head_build_modules: ${{ steps.files.outputs.head_build_modules }} | |
| measure_matrix: ${{ steps.shards.outputs.matrix }} | |
| steps: | |
| - name: Resolve PR number, head SHA, base SHA | |
| id: pr | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| REPO: ${{ github.repository }} | |
| EVENT_NAME: ${{ github.event_name }} | |
| DISPATCH_PR: ${{ inputs.pr_number }} | |
| PR_FROM_PR_EVENT: ${{ github.event.pull_request.number }} | |
| PR_FROM_COMMENT: ${{ github.event.issue.number }} | |
| run: | | |
| set -euo pipefail | |
| case "$EVENT_NAME" in | |
| workflow_dispatch) pr="$DISPATCH_PR" ;; | |
| pull_request) pr="$PR_FROM_PR_EVENT" ;; | |
| issue_comment) pr="$PR_FROM_COMMENT" ;; | |
| *) echo "::error::Unexpected event $EVENT_NAME"; exit 1 ;; | |
| esac | |
| if [ -z "$pr" ]; then echo "::error::Could not resolve PR number"; exit 1; fi | |
| shas=$(gh api "repos/$REPO/pulls/$pr" --jq '"\(.head.sha) \(.base.sha)"') | |
| head_sha=${shas%% *} | |
| base_sha=${shas##* } | |
| { | |
| echo "number=$pr" | |
| echo "head_sha=$head_sha" | |
| echo "base_sha=$base_sha" | |
| } >> "$GITHUB_OUTPUT" | |
| echo "Resolved PR #$pr — head $head_sha, base $base_sha" | |
| - name: Checkout PR head | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| ref: ${{ steps.pr.outputs.head_sha }} | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| # Only checks whether a warm build cache exists (the comparison is | |
| # unaffordable without one); the measurement jobs download it. | |
| - name: Check for a warm build cache | |
| id: lake-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| lookup-only: true | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.pr.outputs.head_sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Determine new and modified Lean files | |
| id: files | |
| env: | |
| BASE_SHA: ${{ steps.pr.outputs.base_sha }} | |
| CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }} | |
| run: | | |
| set -euo pipefail | |
| added=$(git diff --no-renames --name-only --diff-filter=A "$BASE_SHA"...HEAD \ | |
| -- LeanPool \ | |
| | grep '\.lean$' \ | |
| | tr '\n' ' ' || true) | |
| modified=$(git diff --no-renames --name-only --diff-filter=M "$BASE_SHA"...HEAD \ | |
| -- LeanPool \ | |
| | grep '\.lean$' \ | |
| | tr '\n' ' ' || true) | |
| files="${added}${modified}" | |
| merge_base=$(git merge-base "$BASE_SHA" HEAD) | |
| # A base→head comparison is only meaningful when the merge base | |
| # compiles with the same toolchain and dependencies as the head, | |
| # and only affordable when the restored cache already covers most | |
| # of the base build. | |
| compare=false | |
| compare_note="" | |
| if [ -n "$modified" ]; then | |
| if ! git diff --quiet "$merge_base" HEAD -- \ | |
| lean-toolchain lake-manifest.json lakefile.toml; then | |
| compare_note="Base→head comparison skipped: this PR changes the toolchain, manifest, or lakefile, so the two sides would not be comparable." | |
| elif [ -z "$CACHE_MATCHED" ]; then | |
| compare_note="Base→head comparison skipped: no warm build cache was available to build the base affordably." | |
| else | |
| compare=true | |
| fi | |
| fi | |
| # Modified files get the cheap base→head heartbeat comparison, so | |
| # the expensive serial `lean --profile` pass covers only added | |
| # files. Without a comparison, modified files keep the full | |
| # absolute treatment. | |
| if [ "$compare" = true ]; then | |
| profile_files="$added" | |
| else | |
| profile_files="$files" | |
| fi | |
| # Module names for targeted `lake build` (path → dotted module): | |
| # measurement only needs the measured files' imports built, so the | |
| # build targets are the changed modules, never the whole library. | |
| # (The measure shards derive their own module lists from their | |
| # slice of the modified files.) | |
| head_build_modules="" | |
| if [ -n "$profile_files" ]; then | |
| # shellcheck disable=SC2086 # word-split the file list on purpose | |
| head_build_modules=$(printf '%s\n' $profile_files \ | |
| | sed -e 's/\.lean$//' -e 's#/#.#g' | tr '\n' ' ') | |
| fi | |
| { | |
| echo "files=$files" | |
| echo "added=$added" | |
| echo "modified=$modified" | |
| echo "profile_files=$profile_files" | |
| echo "compare=$compare" | |
| echo "compare_note=$compare_note" | |
| echo "merge_base=$merge_base" | |
| echo "head_build_modules=$head_build_modules" | |
| } >> "$GITHUB_OUTPUT" | |
| if [ -z "$files" ]; then | |
| echo "No new or modified Lean files in this diff; report will explain that." | |
| else | |
| echo "Will profile: $files" | |
| echo "Compare against merge base $merge_base: $compare" | |
| fi | |
| # The measure matrix (side × shard) is computed from the diff at run | |
| # time — no static shard list to maintain. When no comparison will run | |
| # the script emits a placeholder entry so the strategy expression still | |
| # parses; the measure job's `if:` skips it. | |
| - name: Plan measurement shards | |
| id: shards | |
| env: | |
| COMPARE: ${{ steps.files.outputs.compare }} | |
| MODIFIED: ${{ steps.files.outputs.modified }} | |
| MERGE_BASE: ${{ steps.files.outputs.merge_base }} | |
| HEAD_SHA: ${{ steps.pr.outputs.head_sha }} | |
| run: | | |
| set -euo pipefail | |
| # Fall back to the checkout's copy while the script has not landed | |
| # on the default branch yet (a `pull_request` run executes the PR | |
| # merge-ref workflow, so the checkout's copy is its lockstep | |
| # partner there anyway). | |
| git show origin/main:scripts/proof-profile/plan-shards.py \ | |
| > "$RUNNER_TEMP/plan-shards.py" \ | |
| || cp scripts/proof-profile/plan-shards.py "$RUNNER_TEMP/plan-shards.py" | |
| matrix=$(python3 "$RUNNER_TEMP/plan-shards.py") | |
| echo "matrix=$matrix" >> "$GITHUB_OUTPUT" | |
| echo "Measure matrix: $matrix" | |
| measure: | |
| needs: plan | |
| if: needs.plan.outputs.compare == 'true' | |
| runs-on: ubuntu-latest | |
| name: Measure ${{ matrix.side }} ${{ matrix.shard }} | |
| strategy: | |
| # One shard failing must not cancel the rest; the report degrades | |
| # gracefully when files are missing from a side. | |
| fail-fast: false | |
| matrix: ${{ fromJSON(needs.plan.outputs.measure_matrix) }} | |
| steps: | |
| - name: Checkout PR head | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| ref: ${{ needs.plan.outputs.head_sha }} | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.head_sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install Mathlib cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Fetch measurement helpers from the default branch | |
| run: | | |
| set -euo pipefail | |
| git show origin/main:scripts/proof-profile/measure-one.sh > "$RUNNER_TEMP/measure-one.sh" | |
| git show origin/main:scripts/proof-profile/measure-heartbeats.sh > "$RUNNER_TEMP/measure-heartbeats.sh" | |
| chmod +x "$RUNNER_TEMP/measure-one.sh" "$RUNNER_TEMP/measure-heartbeats.sh" | |
| - name: Select this shard's slice of the modified files | |
| id: shard | |
| env: | |
| MODIFIED: ${{ needs.plan.outputs.modified }} | |
| SHARD: ${{ matrix.shard }} | |
| SHARD_COUNT: ${{ matrix.shard_count }} | |
| run: | | |
| set -euo pipefail | |
| # Round-robin over the modified list — derived here from the shard | |
| # index rather than passed through the matrix, so job outputs stay | |
| # small on PRs that touch thousands of files. | |
| # shellcheck disable=SC2086 # word-split the file list on purpose | |
| shard_files=$(printf '%s\n' $MODIFIED \ | |
| | awk -v k="$SHARD_COUNT" -v i="$SHARD" '(NR - 1) % k == i' \ | |
| | tr '\n' ' ') | |
| echo "files=$shard_files" >> "$GITHUB_OUTPUT" | |
| # shellcheck disable=SC2086 # word-split the file list on purpose | |
| echo "Shard $SHARD/$SHARD_COUNT measures $(printf '%s\n' $shard_files | wc -l) files" | |
| - name: Build the measurement environment at the merge base | |
| id: base-env | |
| env: | |
| MERGE_BASE: ${{ needs.plan.outputs.merge_base }} | |
| SHARD_FILES: ${{ steps.shard.outputs.files }} | |
| SIDE: ${{ matrix.side }} | |
| SHARD: ${{ matrix.shard }} | |
| run: | | |
| set -euo pipefail | |
| # The restored cache was built from the base branch, so building | |
| # this shard's modules (which pulls in exactly the dependency | |
| # cones its measurements need) is mostly cache hits. | |
| git checkout -f --detach "$MERGE_BASE" | |
| # shellcheck disable=SC2086 # word-split the file list on purpose | |
| modules=$(printf '%s\n' $SHARD_FILES \ | |
| | sed -e 's/\.lean$//' -e 's#/#.#g' | tr '\n' ' ') | |
| ok=true | |
| # shellcheck disable=SC2086 # modules is a space-separated list on purpose | |
| if ! /usr/bin/time -p ~/.elan/bin/lake build $modules 2>&1 \ | |
| | tee "proof-profile-env-build-$SIDE-$SHARD.log"; then | |
| echo "::warning::Merge-base build failed; this shard's $SIDE-side measurements are skipped." | |
| ok=false | |
| fi | |
| echo "ok=$ok" >> "$GITHUB_OUTPUT" | |
| - name: Measure this shard at the ${{ matrix.side }} revision | |
| id: measure | |
| if: steps.base-env.outputs.ok == 'true' | |
| env: | |
| REF: ${{ matrix.ref }} | |
| LOG: ${{ matrix.log }} | |
| SHARD_FILES: ${{ steps.shard.outputs.files }} | |
| run: | | |
| set -euo pipefail | |
| measured=true | |
| # shellcheck disable=SC2086 # SHARD_FILES is a space-separated list on purpose | |
| "$RUNNER_TEMP/measure-heartbeats.sh" "$LOG" "$REF" $SHARD_FILES \ | |
| || { echo "::warning::Measurement failed."; measured=false; rm -f "$LOG"; } | |
| if [ "$measured" = false ]; then | |
| echo "This shard will be missing from the report." | |
| fi | |
| - name: Upload measurements for the report job | |
| if: ${{ !cancelled() }} | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: proof-profile-part-${{ matrix.side }}-${{ matrix.shard }} | |
| path: | | |
| ${{ matrix.log }} | |
| proof-profile-env-build-*.log | |
| if-no-files-found: ignore | |
| absolute: | |
| needs: plan | |
| if: needs.plan.outputs.profile_files != '' | |
| runs-on: ubuntu-latest | |
| name: Profile added files | |
| steps: | |
| - name: Checkout PR head | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| ref: ${{ needs.plan.outputs.head_sha }} | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - name: Restore Lean dependencies | |
| id: dependency-cache | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: | | |
| ~/.elan | |
| .lake/packages | |
| key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} | |
| - name: Restore pool build | |
| uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae | |
| with: | |
| path: .lake/build | |
| key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.head_sha }} | |
| restore-keys: | | |
| LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- | |
| - name: Install Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Install Mathlib cache | |
| run: | | |
| if [ ! -d ".lake/packages/mathlib" ]; then | |
| ~/.elan/bin/lake exe cache get | |
| else | |
| echo "Mathlib already present from cache" | |
| fi | |
| - name: Fetch measurement helpers from the default branch | |
| run: | | |
| set -euo pipefail | |
| git show origin/main:scripts/proof-profile/measure-one.sh > "$RUNNER_TEMP/measure-one.sh" | |
| git show origin/main:scripts/proof-profile/measure-heartbeats.sh > "$RUNNER_TEMP/measure-heartbeats.sh" | |
| chmod +x "$RUNNER_TEMP/measure-one.sh" "$RUNNER_TEMP/measure-heartbeats.sh" | |
| - name: Build the changed modules | |
| env: | |
| HEAD_MODULES: ${{ needs.plan.outputs.head_build_modules }} | |
| run: | | |
| set -euo pipefail | |
| set -o pipefail | |
| # shellcheck disable=SC2086 # HEAD_MODULES is a space-separated list on purpose | |
| /usr/bin/time -p ~/.elan/bin/lake build $HEAD_MODULES 2>&1 | tee proof-profile-build.log | |
| - name: Profile files with lean --profile | |
| env: | |
| FILES: ${{ needs.plan.outputs.profile_files }} | |
| run: | | |
| set -euo pipefail | |
| : > proof-profile.log | |
| # shellcheck disable=SC2086 # FILES is a space-separated list on purpose | |
| for file in $FILES; do | |
| { | |
| echo "## $file" | |
| # Errors here are logged but never fail the job — this is advisory. | |
| set +e | |
| /usr/bin/time -p ~/.elan/bin/lake env lean --profile "$file" | |
| status=$? | |
| set -e | |
| if [ "$status" -ne 0 ]; then | |
| echo "error: profile command exited with status $status" | |
| fi | |
| echo | |
| } >> proof-profile.log 2>&1 | |
| done | |
| - name: Count heartbeats for profiled files | |
| env: | |
| HEAD_SHA: ${{ needs.plan.outputs.head_sha }} | |
| FILES: ${{ needs.plan.outputs.profile_files }} | |
| run: | | |
| set -euo pipefail | |
| # shellcheck disable=SC2086 # FILES is a space-separated list on purpose | |
| "$RUNNER_TEMP/measure-heartbeats.sh" proof-profile-heartbeats.log "$HEAD_SHA" $FILES | |
| - name: Upload profile logs for the report job | |
| if: ${{ !cancelled() }} | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: proof-profile-part-absolute | |
| path: | | |
| proof-profile.log | |
| proof-profile-heartbeats.log | |
| proof-profile-build.log | |
| if-no-files-found: ignore | |
| report: | |
| needs: [plan, measure, absolute] | |
| # Render whatever was measured, even if one side's job failed — the | |
| # renderer degrades gracefully when a log is missing. `!cancelled()` | |
| # keeps this off only when the run was cancelled outright. | |
| if: >- | |
| !cancelled() && needs.plan.result == 'success' | |
| runs-on: ubuntu-latest | |
| name: Report profile | |
| # Only the reporting job receives comment permissions; measurement jobs | |
| # execute PR Lean code with a read-only token. | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| steps: | |
| - name: Checkout PR head | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| ref: ${{ needs.plan.outputs.head_sha }} | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - name: Download measurement logs | |
| if: needs.plan.outputs.files != '' | |
| uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 | |
| with: | |
| pattern: proof-profile-part-* | |
| merge-multiple: true | |
| - name: Render profile summary | |
| if: needs.plan.outputs.files != '' | |
| env: | |
| BASE_SHA: ${{ needs.plan.outputs.base_sha }} | |
| HEAD_SHA: ${{ needs.plan.outputs.head_sha }} | |
| ADDED_FILES: ${{ needs.plan.outputs.added }} | |
| MODIFIED_FILES: ${{ needs.plan.outputs.modified }} | |
| COMPARE: ${{ needs.plan.outputs.compare }} | |
| COMPARE_NOTE: ${{ needs.plan.outputs.compare_note }} | |
| run: | | |
| set -euo pipefail | |
| # Stitch the per-shard measurement logs back into the two per-side | |
| # logs the renderer reads. Order does not matter — the renderer | |
| # keys sections by file path — but zero-padded shard indices keep | |
| # the glob deterministic anyway. | |
| for shard_log in proof-profile-base-heartbeats-*.log; do | |
| if [ -e "$shard_log" ]; then | |
| cat "$shard_log" >> proof-profile-base-heartbeats.log | |
| fi | |
| done | |
| for shard_log in proof-profile-modified-heartbeats-*.log; do | |
| if [ -e "$shard_log" ]; then | |
| cat "$shard_log" >> proof-profile-heartbeats.log | |
| fi | |
| done | |
| git show origin/main:scripts/proof-profile/render.py > "$RUNNER_TEMP/render.py" | |
| # render.py imports statements.py as a sibling module (both fetched | |
| # to $RUNNER_TEMP, which is render.py's script dir and so on | |
| # sys.path). Fall back to the checkout while it has not landed on | |
| # the default branch yet. | |
| git show origin/main:scripts/proof-profile/statements.py \ | |
| > "$RUNNER_TEMP/statements.py" \ | |
| || cp scripts/proof-profile/statements.py "$RUNNER_TEMP/statements.py" | |
| python3 "$RUNNER_TEMP/render.py" | |
| - name: Report no files to profile | |
| if: needs.plan.outputs.files == '' | |
| run: | | |
| cat > proof-profile.md <<'EOF' | |
| ## Proof profile (new / modified Lean files) | |
| No added or modified Lean files under `LeanPool/` in this PR. No compile-cost measurements are needed. | |
| _Advisory only — never blocks merge._ | |
| EOF | |
| cat proof-profile.md >> "$GITHUB_STEP_SUMMARY" | |
| # Same-repo PR runs, `/profile` comments, and dispatches post directly. | |
| # Fork PRs use the artifact companion because their token is read-only. | |
| # The `workflow_run` | |
| # companion cannot cover these reliably: GitHub never emits the event | |
| # for re-run attempts, which silently lost the comment on a bot-opened | |
| # PR whose first attempt sat waiting for approval (#326). | |
| - name: Post sticky PR comment (writable-token runs) | |
| id: direct_post | |
| if: >- | |
| github.event_name != 'pull_request' || | |
| github.event.pull_request.head.repo.full_name == github.repository | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| REPO: ${{ github.repository }} | |
| PR_NUMBER: ${{ needs.plan.outputs.number }} | |
| run: | | |
| set -euo pipefail | |
| if [ ! -f proof-profile.md ]; then | |
| echo "No rendered profile; nothing to post." | |
| exit 0 | |
| fi | |
| # Same marker as the companion workflow, so either poster updates | |
| # the other's comment instead of stacking a duplicate. | |
| marker="<!-- proof-profile-comment -->" | |
| { | |
| printf '%s\n' "$marker" | |
| cat proof-profile.md | |
| } > comment-body.md | |
| existing=$(gh api "repos/$REPO/issues/$PR_NUMBER/comments" --paginate \ | |
| --jq "[.[] | select(.body | startswith(\"$marker\"))] | first | .id // empty") | |
| if [ -n "$existing" ]; then | |
| jq -n --rawfile body comment-body.md '{body: $body}' \ | |
| | gh api -X PATCH "repos/$REPO/issues/comments/$existing" --input - | |
| else | |
| gh pr comment "$PR_NUMBER" --repo "$REPO" --body-file comment-body.md | |
| fi | |
| # Stage a retry payload if the direct post fails. The companion only | |
| # publishes the rendered artifact and never executes PR code. | |
| - name: Stage comment payload for the companion workflow | |
| if: ${{ !cancelled() && steps.direct_post.outcome != 'success' }} | |
| env: | |
| PR_NUMBER: ${{ needs.plan.outputs.number }} | |
| run: | | |
| set -euo pipefail | |
| # proof-profile.md is written by the render step above; the PR number | |
| # is re-validated as numeric by the poster before use. | |
| printf '%s\n' "$PR_NUMBER" > proof-profile-pr.txt | |
| - name: Upload comment payload | |
| if: ${{ !cancelled() && steps.direct_post.outcome != 'success' }} | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: proof-profile-comment | |
| path: | | |
| proof-profile.md | |
| proof-profile-pr.txt | |
| if-no-files-found: ignore | |
| - name: Upload proof profile | |
| if: always() | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 | |
| with: | |
| name: proof-profile | |
| path: | | |
| proof-profile.log | |
| proof-profile-heartbeats.log | |
| proof-profile-build.log | |
| proof-profile-base-heartbeats.log | |
| proof-profile-env-build-*.log | |
| if-no-files-found: ignore |