Skip to content

chore(deps): bump the actions group with 6 updates - #26

Merged
hyperpolymath merged 1 commit into
mainfrom
dependabot/github_actions/actions-2fef39f4b1
Jul 24, 2026
Merged

chore(deps): bump the actions group with 6 updates#26
hyperpolymath merged 1 commit into
mainfrom
dependabot/github_actions/actions-2fef39f4b1

Conversation

@dependabot

@dependabot dependabot Bot commented on behalf of github Jul 24, 2026

Copy link
Copy Markdown
Contributor

Bumps the actions group with 6 updates:

Package From To
actions/checkout 7.0.0 7.0.1
github/codeql-action/init 4.37.1 4.37.3
github/codeql-action/analyze 4.37.1 4.37.3
hyperpolymath/a2ml-validate-action 55e8c28bab4e7f2399fdbd57a6da1051369f3847 0f8081cdfa293663ec6b204274b4272da302e564
hyperpolymath/k9-validate-action 7c3c0e9fa5165626e74ecce78109b3295b798b92 b4b4bd64851e55e003fc756ca706c19f3442e999
dawidd6/action-send-mail c50dc4cc848ade21f848990889906d804fae78c5 12335b969ae3fb71bee5f2c6b829744261aec34c

Updates actions/checkout from 7.0.0 to 7.0.1

Release notes

Sourced from actions/checkout's releases.

v7.0.1

What's Changed

Full Changelog: actions/checkout@v7...v7.0.1

Changelog

Sourced from actions/checkout's changelog.

Changelog

v7.0.1

v7.0.0

v6.0.3

v6.0.2

v6.0.1

v6.0.0

v5.0.1

v5.0.0

v4.3.1

v4.3.0

v4.2.2

v4.2.1

... (truncated)

Commits

Updates github/codeql-action/init from 4.37.1 to 4.37.3

Release notes

Sourced from github/codeql-action/init's releases.

v4.37.3

No user facing changes.

v4.37.2

  • The new address format for the config-file input that was introduced in CodeQL Action 4.37.0 is now enabled by default. In addition to the format described there, the remote= prefix can now be used to explicitly indicate that the input refers to a remote file. All previous input formats continue to be accepted as well. #4023
  • The CodeQL Action can now make use of configured private registries in Default Setup to retrieve CodeQL configuration files from remote repositories that require authentication. This will allow customers to store their CodeQL configuration in a single repository that can then be referenced by Default Setup workflows in other repositories. We expect to roll this and other, related changes out to everyone in July. #4007
Changelog

Sourced from github/codeql-action/init's changelog.

CodeQL Action Changelog

See the releases page for the relevant changes to the CodeQL CLI and language packs.

[UNRELEASED]

No user facing changes.

4.37.3 - 22 Jul 2026

No user facing changes.

4.37.2 - 21 Jul 2026

  • The new address format for the config-file input that was introduced in CodeQL Action 4.37.0 is now enabled by default. In addition to the format described there, the remote= prefix can now be used to explicitly indicate that the input refers to a remote file. All previous input formats continue to be accepted as well. #4023
  • The CodeQL Action can now make use of configured private registries in Default Setup to retrieve CodeQL configuration files from remote repositories that require authentication. This will allow customers to store their CodeQL configuration in a single repository that can then be referenced by Default Setup workflows in other repositories. We expect to roll this and other, related changes out to everyone in July. #4007

4.37.1 - 16 Jul 2026

  • Upcoming breaking change: Add a deprecation warning for customers using CodeQL version 2.20.6 and earlier. These versions of CodeQL were discontinued on 1 July 2026 alongside GitHub Enterprise Server 3.16, and will be unsupported by the next minor release of the CodeQL Action. #3956
  • Update default CodeQL bundle version to 2.26.1. #4019

4.37.0 - 08 Jul 2026

  • Update default CodeQL bundle version to 2.26.0. #3995
  • In addition to the existing input format, the config-file input for the codeql-action/init step will soon support a new [owner/]repo[@ref][:path] format. All components except the repository name are optional. If omitted, owner defaults to the same owner as the repository the analysis is running for, ref to main, and path to .github/codeql-action.yaml. Support for this format ships in this version of the CodeQL Action, but will only be enabled over the coming weeks. #3973

4.36.3 - 01 Jul 2026

No user facing changes.

4.36.2 - 04 Jun 2026

  • Cache CodeQL CLI version information across Actions steps. #3943
  • Reduce requests while waiting for analysis processing by using exponential backoff when polling SARIF processing status. #3937
  • Update default CodeQL bundle version to 2.25.6. #3948

4.36.1 - 02 Jun 2026

No user facing changes.

4.36.0 - 22 May 2026

  • Breaking change: Bump the minimum required CodeQL bundle version to 2.19.4. #3894
  • Add support for SHA-256 Git object IDs. #3893
  • Update default CodeQL bundle version to 2.25.5. #3926

4.35.5 - 15 May 2026

  • We have improved how the JavaScript bundles for the CodeQL Action are generated to avoid duplication across bundles and reduce the size of the repository by around 70%. This should have no effect on the runtime behaviour of the CodeQL Action. #3899

... (truncated)

Commits
  • e4fba86 Merge pull request #4031 from github/update-v4.37.3-72f6a9da0
  • fb50ab5 Update changelog for v4.37.3
  • 72f6a9d Merge pull request #4030 from github/mbg/fix/no-proxy
  • 3b5ee58 Use default request options instead of undefined
  • bfb6be4 Merge pull request #4028 from github/mergeback/v4.37.2-to-main-e0647621
  • 526ab84 Rebuild
  • d6217b9 Update changelog and version after v4.37.2
  • e064762 Merge pull request #4027 from github/update-v4.37.2-385bcdc5a
  • e0faed8 Add a couple of change notes
  • 73aad0e Update changelog for v4.37.2
  • Additional commits viewable in compare view

Updates github/codeql-action/analyze from 4.37.1 to 4.37.3

Release notes

Sourced from github/codeql-action/analyze's releases.

v4.37.3

No user facing changes.

v4.37.2

  • The new address format for the config-file input that was introduced in CodeQL Action 4.37.0 is now enabled by default. In addition to the format described there, the remote= prefix can now be used to explicitly indicate that the input refers to a remote file. All previous input formats continue to be accepted as well. #4023
  • The CodeQL Action can now make use of configured private registries in Default Setup to retrieve CodeQL configuration files from remote repositories that require authentication. This will allow customers to store their CodeQL configuration in a single repository that can then be referenced by Default Setup workflows in other repositories. We expect to roll this and other, related changes out to everyone in July. #4007
Changelog

Sourced from github/codeql-action/analyze's changelog.

CodeQL Action Changelog

See the releases page for the relevant changes to the CodeQL CLI and language packs.

[UNRELEASED]

No user facing changes.

4.37.3 - 22 Jul 2026

No user facing changes.

4.37.2 - 21 Jul 2026

  • The new address format for the config-file input that was introduced in CodeQL Action 4.37.0 is now enabled by default. In addition to the format described there, the remote= prefix can now be used to explicitly indicate that the input refers to a remote file. All previous input formats continue to be accepted as well. #4023
  • The CodeQL Action can now make use of configured private registries in Default Setup to retrieve CodeQL configuration files from remote repositories that require authentication. This will allow customers to store their CodeQL configuration in a single repository that can then be referenced by Default Setup workflows in other repositories. We expect to roll this and other, related changes out to everyone in July. #4007

4.37.1 - 16 Jul 2026

  • Upcoming breaking change: Add a deprecation warning for customers using CodeQL version 2.20.6 and earlier. These versions of CodeQL were discontinued on 1 July 2026 alongside GitHub Enterprise Server 3.16, and will be unsupported by the next minor release of the CodeQL Action. #3956
  • Update default CodeQL bundle version to 2.26.1. #4019

4.37.0 - 08 Jul 2026

  • Update default CodeQL bundle version to 2.26.0. #3995
  • In addition to the existing input format, the config-file input for the codeql-action/init step will soon support a new [owner/]repo[@ref][:path] format. All components except the repository name are optional. If omitted, owner defaults to the same owner as the repository the analysis is running for, ref to main, and path to .github/codeql-action.yaml. Support for this format ships in this version of the CodeQL Action, but will only be enabled over the coming weeks. #3973

4.36.3 - 01 Jul 2026

No user facing changes.

4.36.2 - 04 Jun 2026

  • Cache CodeQL CLI version information across Actions steps. #3943
  • Reduce requests while waiting for analysis processing by using exponential backoff when polling SARIF processing status. #3937
  • Update default CodeQL bundle version to 2.25.6. #3948

4.36.1 - 02 Jun 2026

No user facing changes.

4.36.0 - 22 May 2026

  • Breaking change: Bump the minimum required CodeQL bundle version to 2.19.4. #3894
  • Add support for SHA-256 Git object IDs. #3893
  • Update default CodeQL bundle version to 2.25.5. #3926

4.35.5 - 15 May 2026

  • We have improved how the JavaScript bundles for the CodeQL Action are generated to avoid duplication across bundles and reduce the size of the repository by around 70%. This should have no effect on the runtime behaviour of the CodeQL Action. #3899

... (truncated)

Commits
  • e4fba86 Merge pull request #4031 from github/update-v4.37.3-72f6a9da0
  • fb50ab5 Update changelog for v4.37.3
  • 72f6a9d Merge pull request #4030 from github/mbg/fix/no-proxy
  • 3b5ee58 Use default request options instead of undefined
  • bfb6be4 Merge pull request #4028 from github/mergeback/v4.37.2-to-main-e0647621
  • 526ab84 Rebuild
  • d6217b9 Update changelog and version after v4.37.2
  • e064762 Merge pull request #4027 from github/update-v4.37.2-385bcdc5a
  • e0faed8 Add a couple of change notes
  • 73aad0e Update changelog for v4.37.2
  • Additional commits viewable in compare view

Updates hyperpolymath/a2ml-validate-action from 55e8c28bab4e7f2399fdbd57a6da1051369f3847 to 0f8081cdfa293663ec6b204274b4272da302e564

Changelog

Sourced from hyperpolymath/a2ml-validate-action's changelog.

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

[Unreleased]

[1.0.0] - 2026-05-29

Added

  • Initial Marketplace-ready composite action for validating .a2ml manifests.
  • Configurable path, strict, and paths-ignore inputs.
  • GitHub Actions outputs for scanned files, validation errors, and warnings.

Fixed

  • Allow local smoke runs outside GitHub Actions by defaulting missing GITHUB_OUTPUT to /dev/null.
Commits
  • 0f8081c Sync local commits to main (#61)
  • dea1950 sweep4: add C-A-G-M files
  • cd62208 sweep3: add license files and SPDX identifiers
  • b5d30fb sweep2: add config files (mise.toml)
  • 56f6e4f fix(ci): close the governance gate — SPDX, permissions, SHA pins, reusable bu...
  • 5468b7f security: re-pin secret scanner onto the real gitleaks gate (#59)
  • bafa539 chore(deps): bump the actions group with 4 updates (#58)
  • See full diff in compare view

Updates hyperpolymath/k9-validate-action from 7c3c0e9fa5165626e74ecce78109b3295b798b92 to b4b4bd64851e55e003fc756ca706c19f3442e999

Changelog

Sourced from hyperpolymath/k9-validate-action's changelog.

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

[Unreleased]

[1.0.0] - 2026-05-29

Added

  • Initial Marketplace-ready composite action for validating .k9 and .k9.ncl files.
  • Configurable path, strict, and paths-ignore inputs.
  • GitHub Actions outputs for scanned files, validation errors, and warnings.

Fixed

  • Allow local smoke runs outside GitHub Actions by defaulting missing GITHUB_OUTPUT to /dev/null.
Commits
  • b4b4bd6 fix(ci): estate-wide foundational remediation (#41)
  • c8ec398 fix(ci): estate-wide foundational remediation
  • 91d662e Sync local commits to main (#40)
  • 9643c0a sweep4: add C-A-G-M files
  • 401609c sweep3: add license files and SPDX identifiers
  • ee2abe4 sweep2: add config files (mise.toml)
  • 0aedc05 fix(ci): close the governance gate — SPDX, permissions, SHA pins, reusable bu...
  • 08958c9 security: re-pin secret scanner onto the real gitleaks gate (#38)
  • 01ab911 chore(deps): bump the actions group with 4 updates (#37)
  • See full diff in compare view

Updates dawidd6/action-send-mail from c50dc4cc848ade21f848990889906d804fae78c5 to 12335b969ae3fb71bee5f2c6b829744261aec34c

Commits

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

  • @dependabot rebase will rebase this PR
  • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
  • @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
  • @dependabot ignore <dependency name> major version will close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)
  • @dependabot ignore <dependency name> minor version will close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)
  • @dependabot ignore <dependency name> will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)
  • @dependabot unignore <dependency name> will remove all of the ignore conditions of the specified dependency
  • @dependabot unignore <dependency name> <ignore condition> will remove the ignore condition of the specified dependency and ignore conditions

@dependabot
chore(deps): bump the actions group with 6 updates
f81880e 
Bumps the actions group with 6 updates:

| Package | From | To |
| --- | --- | --- |
| [actions/checkout](https://github.com/actions/checkout) | `7.0.0` | `7.0.1` |
| [github/codeql-action/init](https://github.com/github/codeql-action) | `4.37.1` | `4.37.3` |
| [github/codeql-action/analyze](https://github.com/github/codeql-action) | `4.37.1` | `4.37.3` |
| [hyperpolymath/a2ml-validate-action](https://github.com/hyperpolymath/a2ml-validate-action) | `55e8c28bab4e7f2399fdbd57a6da1051369f3847` | `0f8081cdfa293663ec6b204274b4272da302e564` |
| [hyperpolymath/k9-validate-action](https://github.com/hyperpolymath/k9-validate-action) | `7c3c0e9fa5165626e74ecce78109b3295b798b92` | `b4b4bd64851e55e003fc756ca706c19f3442e999` |
| [dawidd6/action-send-mail](https://github.com/dawidd6/action-send-mail) | `c50dc4cc848ade21f848990889906d804fae78c5` | `12335b969ae3fb71bee5f2c6b829744261aec34c` |


Updates `actions/checkout` from 7.0.0 to 7.0.1
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](actions/checkout@9c091bb...3d3c42e)

Updates `github/codeql-action/init` from 4.37.1 to 4.37.3
- [Release notes](https://github.com/github/codeql-action/releases)
- [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md)
- [Commits](github/codeql-action@7188fc3...e4fba86)

Updates `github/codeql-action/analyze` from 4.37.1 to 4.37.3
- [Release notes](https://github.com/github/codeql-action/releases)
- [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md)
- [Commits](github/codeql-action@7188fc3...e4fba86)

Updates `hyperpolymath/a2ml-validate-action` from 55e8c28bab4e7f2399fdbd57a6da1051369f3847 to 0f8081cdfa293663ec6b204274b4272da302e564
- [Release notes](https://github.com/hyperpolymath/a2ml-validate-action/releases)
- [Changelog](https://github.com/hyperpolymath/a2ml-validate-action/blob/main/CHANGELOG.md)
- [Commits](https://github.com/hyperpolymath/a2ml-validate-action/compare/55e8c28bab4e7f2399fdbd57a6da1051369f3847...0f8081cdfa293663ec6b204274b4272da302e564)

Updates `hyperpolymath/k9-validate-action` from 7c3c0e9fa5165626e74ecce78109b3295b798b92 to b4b4bd64851e55e003fc756ca706c19f3442e999
- [Release notes](https://github.com/hyperpolymath/k9-validate-action/releases)
- [Changelog](https://github.com/hyperpolymath/k9-validate-action/blob/main/CHANGELOG.md)
- [Commits](https://github.com/hyperpolymath/k9-validate-action/compare/7c3c0e9fa5165626e74ecce78109b3295b798b92...b4b4bd64851e55e003fc756ca706c19f3442e999)

Updates `dawidd6/action-send-mail` from c50dc4cc848ade21f848990889906d804fae78c5 to 12335b969ae3fb71bee5f2c6b829744261aec34c
- [Release notes](https://github.com/dawidd6/action-send-mail/releases)
- [Commits](dawidd6/action-send-mail@c50dc4c...12335b9)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 7.0.1
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: actions
- dependency-name: github/codeql-action/init
  dependency-version: 4.37.3
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: actions
- dependency-name: github/codeql-action/analyze
  dependency-version: 4.37.3
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: actions
- dependency-name: hyperpolymath/a2ml-validate-action
  dependency-version: 0f8081cdfa293663ec6b204274b4272da302e564
  dependency-type: direct:production
  dependency-group: actions
- dependency-name: hyperpolymath/k9-validate-action
  dependency-version: b4b4bd64851e55e003fc756ca706c19f3442e999
  dependency-type: direct:production
  dependency-group: actions
- dependency-name: dawidd6/action-send-mail
  dependency-version: 12335b969ae3fb71bee5f2c6b829744261aec34c
  dependency-type: direct:production
  dependency-group: actions
...

Signed-off-by: dependabot[bot] <support@github.com>
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels Jul 24, 2026
@dependabot
dependabot Bot requested a review from hyperpolymath as a code owner July 24, 2026 07:08
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels Jul 24, 2026
@sonarqubecloud

sonarqubecloud Bot commented Jul 24, 2026

Copy link
Copy Markdown

Quality Gate Passed Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

@hyperpolymath
hyperpolymath merged commit 0be2ae3 into main Jul 24, 2026
1 check passed
@hyperpolymath
hyperpolymath deleted the dependabot/github_actions/actions-2fef39f4b1 branch July 24, 2026 08:41
hyperpolymath added a commit that referenced this pull request Jul 27, 2026
@hyperpolymath @claude
Merge origin/main into proofs/lean4-l1-l2 (pre-PR sync)
0104c9c 
Brings the branch up to date with main (was 14 behind) so the ET-2 proof can
be promoted to main with a green check roster.

Five conflicts, all resolved by inspection rather than a blanket --ours/--theirs.
Four were add/add artefacts of main having received a SQUASHED copy of this
branch via PR #17, which makes git see both sides as independent additions:

  MANIFEST, Systemet.lean, Systemet/Audit.lean
    Verified main's content is byte-identical to the branch's and the branch
    is a strict superset (adds exactly the four ET-2 entries/imports/audit
    lines). Took the branch side.

  docs/status/PROOF-STATUS.adoc
    Every difference is this branch's ET-2 update (gated 11 -> 15, ET-2 row
    proven, MECH-1 row landed, stale "ET-2 (finish)" OPEN row dropped); main
    carried no independent edits. Took the branch side.

  .github/workflows/proofs.yml
    Genuine two-sided merge -- the two sides differ in OPPOSITE directions:
      main   has actions/checkout@3d3c42e (v7.0.1, from dependabot #26)
      branch has curl --proto '=https' --tlsv1.2 (Sonar S6506 fix, 1f2a81a)
    Took main's newer pin and re-applied the branch's https hardening on top,
    so neither is regressed. Both verified present after resolution.

Verified on the merged tree (measured, not assumed):
  cold rebuild (rm -rf .lake/build)  Build completed successfully (16 jobs)
  scripts/check-proofs.sh lean4      PASS, real exit 0
                                     audit 20/20 in the trusted base
  scripts/scan-dangerous.sh          PASS, real exit 0
  scripts/check-proof-status.sh      PASS, real exit 0 (15 gated, doc agrees)
  forbidden-token scan on the four new proof files: clean

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@hyperpolymath hyperpolymath mentioned this pull request Jul 27, 2026
Merged
hyperpolymath added a commit that referenced this pull request Jul 27, 2026
@hyperpolymath
proofs(lean4): promote ET-2 to main — L1 conversion is decidable (#27)
eed2092 
Promotes the **ET-2 closure** (decidability of L1 conversion) onto
`main`.

## Why this PR exists

ET-2 was proven and merged in **PR #24** — but into
`proofs/lean4-l1-l2`, **not `main`**. PR #17 had squash-merged that
branch to `main` *before* ET-2 existed, so `main` holds the L1/L2
mechanization content while the ET-2 work sits only on the branch. No
second PR to `main` was ever opened.

Measured before this PR: `main...proofs/lean4-l1-l2` was **diverged, 4
ahead / 14 behind**, and all four ET-2 proof files returned **404 on
`main`**. Anything reading `main` today correctly concludes ET-2 is
still open.

## What lands on `main`

| File | Contents |
|---|---|
| `Systemet/L1/SubstLemmas.lean` | substitution/weakening exchange
family, incl. `nf_substTy` — normalization commutes with hereditary
substitution (the whole content of the β case) |
| `Systemet/L1/Soundness.lean` | `soundness : DefEq t (embNf (nf t))` |
| `Systemet/L1/Completeness.lean` | `completeness : DefEq t u → nf t =
nf u`; `defEq_iff_nf : DefEq t u ↔ nf t = nf u` |
| `Systemet/L1/Decidable.lean` | `decEqNf` / `decEqSp` (hand-rolled
mutual `DecidableEq` — `deriving` does not work across the `Nf`/`Sp`
pair); `decDefEq : (t u : Ty Γ k) → Decidable (DefEq t u)` |

Plus the `PROOF-STATUS.adoc` truth pass (`gated` 11 → 15, ET-2 row
proven, MECH-1 row landed, the satisfied `ET-2 (finish)` OPEN row
removed) and append-only `MANIFEST` / `Systemet.lean` / `Audit.lean`
entries.

## Conflict resolution — read this bit

The pre-PR sync merge (`0104c9c`) hit five conflicts. **Four were
`add/add` artefacts of the squash in #17**, which makes git treat both
sides as independent additions. None were resolved by a blanket
`--ours`/`--theirs`:

- `MANIFEST`, `Systemet.lean`, `Audit.lean` — verified `main`'s content
is **byte-identical** to the branch's and the branch is a **strict
superset** (adds exactly the four ET-2 entries). Branch side taken.
- `PROOF-STATUS.adoc` — every difference is this branch's ET-2 update;
`main` carried no independent edits. Branch side taken.
- **`.github/workflows/proofs.yml` — a genuine two-sided merge.** The
sides differed in *opposite* directions: `main` had the newer
`actions/checkout@3d3c42e` (v7.0.1, from dependabot #26) while the
branch had `curl --proto '=https' --tlsv1.2` (the Sonar S6506 fix). Took
main's newer pin **and** re-applied the branch's https hardening, so
neither is regressed. Both confirmed present post-resolution.

## Evidence (measured on the merged tree, not inherited from #24)

- Cold rebuild after `rm -rf .lake/build` → **Build completed
successfully (16 jobs)**
- `scripts/check-proofs.sh lean4` → **PASS** (real exit 0); audit
reports **20/20 headline items within the trusted base**
- `scripts/scan-dangerous.sh` → **PASS** (real exit 0)
- `scripts/check-proof-status.sh` → **PASS** (real exit 0) — 15 gated,
document agrees
- Forbidden-token scan on the four new proof files → clean
- `#print axioms` on `soundness`, `completeness`, `defEq_iff_nf`,
`decDefEq`, `decEqNf`, `decEqSp`, `nf_substTy` → **`[propext,
Quot.sound]` only**; no `sorryAx`, no user axioms, not even
`Classical.choice`

Real exit codes were checked directly — piping a gate through `tail` and
reading `$?` reports *tail's* status, which is how a red gate can look
green.

## Scope — what this does *not* claim

`DefEq` here is **β + equivalence + congruence. η is not included** and
remains an OPEN row. **ET-3 is unaffected** — its η and model directions
stay open. `PROOF-STATUS.adoc` marks ET-2 proven *for the L1 core
calculus*, under the core-vs-full-theory caveat that file already
carries.

**ET-14 (TEA erasure) is untouched and remains the headline open
problem**, gated on the owner's ET-16 / L0-lowering ADR.

## Merge notes

Per the base ruleset, **squash is the only merge that works** here
(rebase merges cannot be signed by GitHub bots), and the phantom
required `Dependabot` context means this will need `--admin`. Not merged
by me — that call is yours.

🤖 Generated with [Claude Code](https://claude.com/claude-code)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hyperpolymath hyperpolymath hyperpolymath approved these changes

Assignees

No one assigned

Labels

dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@hyperpolymath