From be3f8f23045aefae5f70ba2e068a6c2091d6ac92 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:29:03 -0700 Subject: [PATCH 1/6] ci: add concise A261865 AXLE diagnostics --- .../workflows/a261865-axle-diagnostics.yml | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 .github/workflows/a261865-axle-diagnostics.yml diff --git a/.github/workflows/a261865-axle-diagnostics.yml b/.github/workflows/a261865-axle-diagnostics.yml new file mode 100644 index 00000000..d23468d6 --- /dev/null +++ b/.github/workflows/a261865-axle-diagnostics.yml @@ -0,0 +1,87 @@ +name: A261865 concise AXLE diagnostics + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/a261865-axle-diagnostics.yml' + - 'audits/a261865-axle-diagnostics.trigger' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: a261865-axle-diagnostics-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +jobs: + axle-diagnostics: + name: Concise AXLE diagnostics + runs-on: ubuntu-slim + timeout-minutes: 25 + steps: + - name: Checkout pinned A261865 proof commit + uses: actions/checkout@v4 + with: + repository: DomTheDeveloper/formal-conjectures + ref: 02688846b7a0d44e208cef7581bbdbb3978813c6 + + - name: Run AXLE and print only actionable diagnostics + shell: bash + run: | + python3 - <<'PY' + import json + import pathlib + import sys + import urllib.request + + files = [ + 'FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean', + 'FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean', + ] + all_results = {} + failed = False + for filename in files: + payload = json.dumps({ + 'content': pathlib.Path(filename).read_text(), + 'environment': 'lean-4.27.0', + 'ignore_imports': False, + 'mathlib_options': False, + 'timeout_seconds': 900, + }).encode() + request = urllib.request.Request( + 'https://axle.axiommath.ai/api/v1/check', + data=payload, + headers={'Content-Type': 'application/json'}, + method='POST', + ) + with urllib.request.urlopen(request, timeout=960) as response: + result = json.load(response) + all_results[filename] = result + errors = result.get('lean_messages', {}).get('errors', []) + warnings = result.get('lean_messages', {}).get('warnings', []) + tool_errors = result.get('tool_messages', {}).get('errors', []) + declarations = result.get('failed_declarations', []) + okay = bool(result.get('okay', False)) + print(f'===== {filename} =====') + print(f'okay={okay}') + print('lean_errors=' + json.dumps(errors, ensure_ascii=False)) + print('tool_errors=' + json.dumps(tool_errors, ensure_ascii=False)) + print('failed_declarations=' + json.dumps(declarations, ensure_ascii=False)) + print('warnings=' + json.dumps(warnings[:10], ensure_ascii=False)) + failed |= bool(errors or tool_errors or declarations or not okay) + pathlib.Path('a261865-axle-results.json').write_text( + json.dumps(all_results, indent=2, ensure_ascii=False) + ) + if failed: + sys.exit(1) + PY + + - name: Upload full AXLE response + if: always() + uses: actions/upload-artifact@v4 + with: + name: a261865-axle-diagnostics + path: a261865-axle-results.json + if-no-files-found: warn From 660551cbc377c192475af498c6c0558171ae6ded Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:29:09 -0700 Subject: [PATCH 2/6] ci: trigger concise A261865 AXLE diagnostics --- audits/a261865-axle-diagnostics.trigger | 1 + 1 file changed, 1 insertion(+) create mode 100644 audits/a261865-axle-diagnostics.trigger diff --git a/audits/a261865-axle-diagnostics.trigger b/audits/a261865-axle-diagnostics.trigger new file mode 100644 index 00000000..5dbd4fdc --- /dev/null +++ b/audits/a261865-axle-diagnostics.trigger @@ -0,0 +1 @@ +02688846b7a0d44e208cef7581bbdbb3978813c6 From 5743ed8c5ba66bba26eb37443ae24b1614e2198f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:33:34 -0700 Subject: [PATCH 3/6] ci: repin A261865 AXLE diagnostics to repaired proof --- .github/workflows/a261865-axle-diagnostics.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/a261865-axle-diagnostics.yml b/.github/workflows/a261865-axle-diagnostics.yml index d23468d6..21962e1e 100644 --- a/.github/workflows/a261865-axle-diagnostics.yml +++ b/.github/workflows/a261865-axle-diagnostics.yml @@ -25,7 +25,7 @@ jobs: uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 02688846b7a0d44e208cef7581bbdbb3978813c6 + ref: 024bf36395a5b19464c43c232450b1ae6230700b - name: Run AXLE and print only actionable diagnostics shell: bash From 4bae2c481e782f6140ba58c53a4311ab27b0367f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:36:06 -0700 Subject: [PATCH 4/6] ci: repin AXLE diagnostics to second repaired proof --- .github/workflows/a261865-axle-diagnostics.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/a261865-axle-diagnostics.yml b/.github/workflows/a261865-axle-diagnostics.yml index 21962e1e..5530ae84 100644 --- a/.github/workflows/a261865-axle-diagnostics.yml +++ b/.github/workflows/a261865-axle-diagnostics.yml @@ -25,7 +25,7 @@ jobs: uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 024bf36395a5b19464c43c232450b1ae6230700b + ref: 7a073b94596edcdf6a3c4c56079e0a75ae404474 - name: Run AXLE and print only actionable diagnostics shell: bash From 5a53f988bc6dd5965182b2220b39badf1e0dfb54 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:37:47 -0700 Subject: [PATCH 5/6] ci: track active A261865 repair branch in AXLE diagnostics --- .github/workflows/a261865-axle-diagnostics.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/a261865-axle-diagnostics.yml b/.github/workflows/a261865-axle-diagnostics.yml index 5530ae84..8153de2d 100644 --- a/.github/workflows/a261865-axle-diagnostics.yml +++ b/.github/workflows/a261865-axle-diagnostics.yml @@ -21,11 +21,11 @@ jobs: runs-on: ubuntu-slim timeout-minutes: 25 steps: - - name: Checkout pinned A261865 proof commit + - name: Checkout current A261865 proof branch uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 7a073b94596edcdf6a3c4c56079e0a75ae404474 + ref: a261865-research - name: Run AXLE and print only actionable diagnostics shell: bash From 28367e62c2e9f0d372f483cc4a0cc42e83adfc76 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:58:15 -0700 Subject: [PATCH 6/6] ci: expand A261865 AXLE diagnostics to support modules --- .github/workflows/a261865-axle-diagnostics.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/a261865-axle-diagnostics.yml b/.github/workflows/a261865-axle-diagnostics.yml index 8153de2d..dd8475b0 100644 --- a/.github/workflows/a261865-axle-diagnostics.yml +++ b/.github/workflows/a261865-axle-diagnostics.yml @@ -19,7 +19,7 @@ jobs: axle-diagnostics: name: Concise AXLE diagnostics runs-on: ubuntu-slim - timeout-minutes: 25 + timeout-minutes: 40 steps: - name: Checkout current A261865 proof branch uses: actions/checkout@v4 @@ -37,8 +37,10 @@ jobs: import urllib.request files = [ - 'FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean', - 'FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean', + 'FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean', ] all_results = {} failed = False @@ -70,7 +72,7 @@ jobs: print('tool_errors=' + json.dumps(tool_errors, ensure_ascii=False)) print('failed_declarations=' + json.dumps(declarations, ensure_ascii=False)) print('warnings=' + json.dumps(warnings[:10], ensure_ascii=False)) - failed |= bool(errors or tool_errors or declarations or not okay) + failed |= bool(errors or tool_errors or not okay) pathlib.Path('a261865-axle-results.json').write_text( json.dumps(all_results, indent=2, ensure_ascii=False) ) @@ -82,6 +84,6 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: a261865-axle-diagnostics + name: a261865-axle-support-diagnostics path: a261865-axle-results.json if-no-files-found: warn