Skip to content

Qualify the two remaining compact cutoff control repairs #426

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
d6g8k5htny-coder wants to merge 1 commit into
base: codex/compact-cutoff-controls-repair-20261011-root01a11cbf
Choose a base branch
from
Draft

Qualify the two remaining compact cutoff control repairs #426

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
286 changes: 286 additions & 0 deletions .github/workflows/compact-cutoff-controls-final-repair.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,286 @@
name: Compact cutoff controls final repair hosted proof check

'on':
pull_request:
types: [opened, synchronize, reopened]
paths:
- 'frontiers/compact_source_cutoff_controls_final_repair_20261011/**'
- '.github/workflows/compact-cutoff-controls-final-repair.yml'

permissions:
contents: read

concurrency:
group: compact-cutoff-controls-final-repair-${{ github.ref }}
cancel-in-progress: false

jobs:
first-leaf:
runs-on: ubuntu-latest
timeout-minutes: 30
env:
LEAN_NUM_THREADS: '2'
EXPECTED_SOURCE_LIST_SHA256: '8d024d0f9e97a9527d8ff1e6ec22d9f12944a07af5d8b4e0112de646e4e1f050'
EXPECTED_BASE_REF: 'codex/compact-cutoff-controls-repair-20261011-root01a11cbf'
defaults:
run:
shell: bash
working-directory: frontiers/compact_source_cutoff_controls_final_repair_20261011
steps:
- name: Record selected event context before checkout
timeout-minutes: 1
working-directory: ${{ runner.temp }}
env:
EVENT_ACTION: ${{ github.event.action }}
EVENT_NUMBER: ${{ github.event.pull_request.number }}
EVENT_HEAD: ${{ github.event.pull_request.head.sha }}
EVENT_BASE: ${{ github.event.pull_request.base.ref }}
EVENT_BASE_SHA: ${{ github.event.pull_request.base.sha }}
run: |
set -euo pipefail
evidence_dir="$RUNNER_TEMP/compact-cutoff-controls-final-repair-precheckout"
mkdir -p "$evidence_dir"
date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/start-utc.txt"
printf 'run=%s\nattempt=%s\nevent=%s\naction=%s\npr=%s\nref=%s\nevent_head=%s\nevent_base=%s\nevent_base_sha=%s\nexpected_merge_sha=%s\nthreads=%s\ncheckout_status=NOT_ESTABLISHED\n' "$GITHUB_RUN_ID" "$GITHUB_RUN_ATTEMPT" "$GITHUB_EVENT_NAME" "$EVENT_ACTION" "$EVENT_NUMBER" "$GITHUB_REF" "$EVENT_HEAD" "$EVENT_BASE" "$EVENT_BASE_SHA" "$GITHUB_SHA" "$LEAN_NUM_THREADS" > "$evidence_dir/context.txt"
- timeout-minutes: 1
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
id: checkout
with:
fetch-depth: 2
persist-credentials: false
- name: Validate one fresh admitted source checkout before setup
timeout-minutes: 1
id: sources
env:
EVENT_ACTION: ${{ github.event.action }}
EVENT_NUMBER: ${{ github.event.pull_request.number }}
EVENT_HEAD: ${{ github.event.pull_request.head.sha }}
EVENT_BASE: ${{ github.event.pull_request.base.ref }}
EVENT_BASE_SHA: ${{ github.event.pull_request.base.sha }}
run: |
set -euo pipefail
mkdir -p .lake/evidence
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/start-utc.txt
git rev-parse HEAD > .lake/evidence/checkout-sha.txt
git rev-parse HEAD^{tree} > .lake/evidence/checkout-tree.txt
git rev-parse HEAD^1 > .lake/evidence/checkout-base-parent.txt
git rev-parse HEAD^2 > .lake/evidence/checkout-head-parent.txt
printf 'event=%s\naction=%s\npr=%s\nref=%s\nhead=%s\nbase=%s\nbase_sha=%s\nmerge=%s\nrun=%s\nattempt=%s\nthreads=%s\n' "$GITHUB_EVENT_NAME" "$EVENT_ACTION" "$EVENT_NUMBER" "$GITHUB_REF" "$EVENT_HEAD" "$EVENT_BASE" "$EVENT_BASE_SHA" "$GITHUB_SHA" "$GITHUB_RUN_ID" "$GITHUB_RUN_ATTEMPT" "$LEAN_NUM_THREADS" > .lake/evidence/context.txt
test "$(date -u +%s)" -lt "$(date -u -d '2026-10-11T17:20:00Z' +%s)"
test "$GITHUB_EVENT_NAME" = pull_request
test "$GITHUB_RUN_ATTEMPT" = 1
case "$EVENT_ACTION" in opened|synchronize|reopened) ;; *) exit 81 ;; esac
[[ "$EVENT_NUMBER" =~ ^[0-9]+$ ]]
test "$GITHUB_REF" = "refs/pull/$EVENT_NUMBER/merge"
test "$EVENT_BASE" = "$EXPECTED_BASE_REF"
[[ "$EVENT_HEAD" =~ ^[0-9a-f]{40}$ ]]
[[ "$EVENT_BASE_SHA" =~ ^[0-9a-f]{40}$ ]]
test "$(cat .lake/evidence/checkout-sha.txt)" = "$GITHUB_SHA"
test "$(cat .lake/evidence/checkout-base-parent.txt)" = "$EVENT_BASE_SHA"
test "$(cat .lake/evidence/checkout-head-parent.txt)" = "$EVENT_HEAD"
[[ "$EXPECTED_SOURCE_LIST_SHA256" =~ ^[0-9a-f]{64}$ ]]
test ! -e .lake/build
command -v jq timeout sha256sum cmp awk
printf 'leanprover/lean4:v4.34.1\n' | cmp -s - lean-toolchain
test "$(wc -l < SOURCE_SHA256SUMS)" -gt 0
if grep -Evq '^[0-9a-f]{64} [A-Za-z0-9._/-]+$' SOURCE_SHA256SUMS; then exit 82; fi
cp SOURCE_SHA256SUMS .lake/evidence/SOURCE_SHA256SUMS
sha256sum SOURCE_SHA256SUMS > .lake/evidence/checksum-list-identity-before.txt
test "$(sha256sum SOURCE_SHA256SUMS | cut -d' ' -f1)" = "$EXPECTED_SOURCE_LIST_SHA256"
grep -Fxq '#print axioms SourceCompactCutoff.compact_cutoff_of_geometry' LeafAxiomAudit.lean
grep -Fxq '#print axioms SourceCompactCutoff.actual_source_compact_cutoff' LeafAxiomAudit.lean
sha256sum -c SOURCE_SHA256SUMS | tee .lake/evidence/sources-before.txt
while IFS= read -r line; do
file="${line#* }"
test "$file" != "$line"
sha256sum -- "$file"
done < SOURCE_SHA256SUMS > .lake/evidence/sources-actual-before.sha256
git diff --exit-code
- name: Install pinned Lean and retrieve qualified Mathlib cache
timeout-minutes: 3
id: setup
uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865
with:
lake-package-directory: frontiers/compact_source_cutoff_controls_final_repair_20261011
auto-config: 'false'
build: 'false'
test: 'false'
lint: 'false'
use-mathlib-cache: 'true'
use-github-cache: 'false'
- name: Check hosted versions pins and actual post-setup source hashes
timeout-minutes: 1
id: pincheck
run: |
set -euo pipefail
lean --version | tee .lake/evidence/lean-version.txt
grep -Eq '^Lean \(version 4\.34\.1([, ]|\))' .lake/evidence/lean-version.txt
lake --version | tee .lake/evidence/lake-version.txt
grep -Fxq 'Lake version 5.0.0-src+5045d00 (Lean version 4.34.1)' .lake/evidence/lake-version.txt
jq --version > .lake/evidence/jq-version.txt
uname -a > .lake/evidence/platform.txt
cp lake-manifest.json .lake/evidence/lake-manifest.json
sha256sum lake-manifest.json > .lake/evidence/manifest-identity.txt
sha256sum SOURCE_SHA256SUMS > .lake/evidence/checksum-list-identity-after-setup.txt
cmp -s .lake/evidence/checksum-list-identity-before.txt .lake/evidence/checksum-list-identity-after-setup.txt
sha256sum -c SOURCE_SHA256SUMS > .lake/evidence/sources-after-setup.txt
while IFS= read -r line; do
file="${line#* }"
test "$file" != "$line"
sha256sum -- "$file"
done < SOURCE_SHA256SUMS > .lake/evidence/sources-actual-after-setup.sha256
cmp -s .lake/evidence/sources-actual-before.sha256 .lake/evidence/sources-actual-after-setup.sha256
jq -r '.packages[] | [.name, .rev] | @tsv' lake-manifest.json > .lake/evidence/dependency-expected.tsv
test "$(wc -l < .lake/evidence/dependency-expected.tsv)" -eq 9
cat > .lake/evidence/dependency-pins-required.tsv <<'PINS'
plausible 118aa17ee84656b8bd727fef7c458ee8c833385c
LeanSearchClient ddf04cf3949fa556442341e87d47f9f6e6074707
importGraph e928b72544873815af278d38681b31c0293588e3
proofwidgets 106ff4fafc74ef4ac99d81dbf3ab399118f497a5
aesop 355695d523e41d0554926416cba2a2b3544fbbc9
Qq 6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259
batteries f2effa3d803fda822b1f97b806c47cf2adfbcbc2
Cli e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204
mathlib d13f23b723b8a846827a245b89c10fc7d3f11612
PINS
cmp -s .lake/evidence/dependency-pins-required.tsv .lake/evidence/dependency-expected.tsv
while IFS=$'\t' read -r package revision; do
actual=$(git -C ".lake/packages/$package" rev-parse HEAD)
printf '%s\t%s\t%s\n' "$package" "$revision" "$actual" >> .lake/evidence/dependency-actual.tsv
test "$actual" = "$revision"
done < .lake/evidence/dependency-expected.tsv
git diff --exit-code
- name: Build fresh project predecessor PushedHeight once
timeout-minutes: 10
id: predecessor
run: |
set -euo pipefail
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/predecessor-start.txt
phase_start=$SECONDS
set +e
timeout --signal=TERM --kill-after=15s 540s lake build PushedHeight > .lake/evidence/predecessor.stdout 2> .lake/evidence/predecessor.stderr
status=$?
set -e
printf '%s\n' "$status" > .lake/evidence/predecessor-exit.txt
printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/predecessor-seconds.txt
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/predecessor-end.txt
cat .lake/evidence/predecessor.stdout
cat .lake/evidence/predecessor.stderr >&2
exit "$status"
- name: Compile first-leaf proof source and propagate actual exit
timeout-minutes: 2
id: proof
run: |
set -euo pipefail
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/proof-start.txt
phase_start=$SECONDS
set +e
timeout --signal=TERM --kill-after=15s 90s lake build CompactSourceCutoffProof > .lake/evidence/proof.stdout 2> .lake/evidence/proof.stderr
status=$?
set -e
printf '%s\n' "$status" > .lake/evidence/proof-exit.txt
printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/proof-seconds.txt
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/proof-end.txt
cat .lake/evidence/proof.stdout
cat .lake/evidence/proof.stderr >&2
exit "$status"
- name: Compile substantive compact-cutoff controls and propagate actual exit
timeout-minutes: 2
id: controls
run: |
set -euo pipefail
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/controls-start.txt
phase_start=$SECONDS
set +e
timeout --signal=TERM --kill-after=15s 90s lake build CompactSourceCutoffControls > .lake/evidence/controls.stdout 2> .lake/evidence/controls.stderr
status=$?
set -e
printf '%s\n' "$status" > .lake/evidence/controls-exit.txt
printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/controls-seconds.txt
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/controls-end.txt
cat .lake/evidence/controls.stdout
cat .lake/evidence/controls.stderr >&2
exit "$status"
- name: Recheck both compiled modules with the standalone kernel checker
id: kernel
timeout-minutes: 2
run: |
set -euo pipefail
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/kernel-start.txt
phase_start=$SECONDS
set +e
timeout --signal=TERM --kill-after=15s 90s bash -c 'set -euo pipefail; printf "KERNEL_MODULE CompactSourceCutoffProof\n"; lake env leanchecker CompactSourceCutoffProof; printf "KERNEL_MODULE CompactSourceCutoffControls\n"; lake env leanchecker CompactSourceCutoffControls' > .lake/evidence/kernel.stdout 2> .lake/evidence/kernel.stderr
status=$?
set -e
printf '%s\n' "$status" > .lake/evidence/kernel-exit.txt
printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/kernel-seconds.txt
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/kernel-end.txt
cat .lake/evidence/kernel.stdout
cat .lake/evidence/kernel.stderr >&2
exit "$status"
- name: Audit all new declarations and propagate actual audit exit
timeout-minutes: 2
id: audit
run: |
set -euo pipefail
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/audit-start.txt
phase_start=$SECONDS
set +e
timeout --signal=TERM --kill-after=15s 90s lake env lean LeafAxiomAudit.lean > .lake/evidence/audit.stdout 2> .lake/evidence/audit.stderr
status=$?
set -e
printf '%s\n' "$status" > .lake/evidence/audit-exit.txt
printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/audit-seconds.txt
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/audit-end.txt
cat .lake/evidence/audit.stdout
cat .lake/evidence/audit.stderr >&2
exit "$status"
- name: Retain checkout and phase outcomes even if checkout fails
timeout-minutes: 1
if: always()
working-directory: ${{ runner.temp }}
env:
CHECKOUT_OUTCOME: ${{ steps.checkout.outcome }}
SOURCE_OUTCOME: ${{ steps.sources.outcome }}
SETUP_OUTCOME: ${{ steps.setup.outcome }}
PINCHECK_OUTCOME: ${{ steps.pincheck.outcome }}
PREDECESSOR_OUTCOME: ${{ steps.predecessor.outcome }}
PROOF_OUTCOME: ${{ steps.proof.outcome }}
CONTROLS_OUTCOME: ${{ steps.controls.outcome }}
KERNEL_OUTCOME: ${{ steps.kernel.outcome }}
AUDIT_OUTCOME: ${{ steps.audit.outcome }}
run: |
set -euo pipefail
evidence_dir="$RUNNER_TEMP/compact-cutoff-controls-final-repair-precheckout"
mkdir -p "$evidence_dir"
date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/end-utc.txt"
printf 'checkout=%s\nsources=%s\nsetup=%s\npincheck=%s\npredecessor=%s\nproof=%s\ncontrols=%s\nkernel=%s\naudit=%s\nscientific_effect=NONE\n' "$CHECKOUT_OUTCOME" "$SOURCE_OUTCOME" "$SETUP_OUTCOME" "$PINCHECK_OUTCOME" "$PREDECESSOR_OUTCOME" "$PROOF_OUTCOME" "$CONTROLS_OUTCOME" "$KERNEL_OUTCOME" "$AUDIT_OUTCOME" > "$evidence_dir/outcomes.txt"
- name: Retain final exact source and tracked-tree integrity
timeout-minutes: 1
if: ${{ always() && steps.checkout.outcome == 'success' }}
run: |
set -euo pipefail
mkdir -p .lake/evidence
date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/end-utc.txt
sha256sum SOURCE_SHA256SUMS > .lake/evidence/checksum-list-identity-final.txt
cmp -s .lake/evidence/checksum-list-identity-before.txt .lake/evidence/checksum-list-identity-final.txt
sha256sum -c SOURCE_SHA256SUMS > .lake/evidence/sources-final.txt
while IFS= read -r line; do
file="${line#* }"
test "$file" != "$line"
sha256sum -- "$file"
done < SOURCE_SHA256SUMS > .lake/evidence/sources-actual-final.sha256
cmp -s .lake/evidence/sources-actual-before.sha256 .lake/evidence/sources-actual-final.sha256
git diff --exit-code > .lake/evidence/tracked-tree-final.txt
- name: Preserve complete phase logs on success or failure
timeout-minutes: 1
if: always()
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
with:
name: compact-cutoff-controls-final-repair-${{ github.run_id }}-${{ github.run_attempt }}
path: |
frontiers/compact_source_cutoff_controls_final_repair_20261011/.lake/evidence/
${{ runner.temp }}/compact-cutoff-controls-final-repair-precheckout/
include-hidden-files: true
if-no-files-found: error
retention-days: 14
1 change: 1 addition & 0 deletions frontiers/compact_source_cutoff_controls_final_repair_20261011/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
.lake/
Loading
Loading