chore(deps): bump the actions group across 1 directory with 10 updates#2
Closed
dependabot[bot] wants to merge 1 commit into
Closed
chore(deps): bump the actions group across 1 directory with 10 updates#2dependabot[bot] wants to merge 1 commit into
dependabot[bot] wants to merge 1 commit into
Conversation
Bumps the actions group with 10 updates in the / directory: | Package | From | To | | --- | --- | --- | | [actions/checkout](https://github.com/actions/checkout) | `4.1.1` | `6.0.2` | | [haskell-actions/setup](https://github.com/haskell-actions/setup) | `2.7.5` | `2.10.3` | | [actions/cache](https://github.com/actions/cache) | `4.0.2` | `5.0.3` | | [actions/upload-pages-artifact](https://github.com/actions/upload-pages-artifact) | `3.0.1` | `4.0.0` | | [github/codeql-action](https://github.com/github/codeql-action) | `3.27.0` | `4.32.0` | | [erlef/setup-beam](https://github.com/erlef/setup-beam) | `1.17.5` | `1.20.4` | | [actions/github-script](https://github.com/actions/github-script) | `7.0.1` | `8.0.0` | | [webfactory/ssh-agent](https://github.com/webfactory/ssh-agent) | `0.9.0` | `0.9.1` | | [Swatinem/rust-cache](https://github.com/swatinem/rust-cache) | `ad397744b0d591a723ab90405b7247fac0e6b8db` | `779680da715d629ac1d338a641029a2f4372abb5` | | [ossf/scorecard-action](https://github.com/ossf/scorecard-action) | `2.4.0` | `2.4.3` | Updates `actions/checkout` from 4.1.1 to 6.0.2 - [Release notes](https://github.com/actions/checkout/releases) - [Commits](actions/checkout@v4.1.1...v6.0.2) Updates `haskell-actions/setup` from 2.7.5 to 2.10.3 - [Release notes](https://github.com/haskell-actions/setup/releases) - [Commits](haskell-actions/setup@ec49483...f9150cb) Updates `actions/cache` from 4.0.2 to 5.0.3 - [Release notes](https://github.com/actions/cache/releases) - [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md) - [Commits](actions/cache@0c45773...cdf6c1f) Updates `actions/upload-pages-artifact` from 3.0.1 to 4.0.0 - [Release notes](https://github.com/actions/upload-pages-artifact/releases) - [Commits](actions/upload-pages-artifact@56afc60...7b1f4a7) Updates `github/codeql-action` from 3.27.0 to 4.32.0 - [Release notes](https://github.com/github/codeql-action/releases) - [Commits](github/codeql-action@v3.27.0...v4.32.0) Updates `erlef/setup-beam` from 1.17.5 to 1.20.4 - [Release notes](https://github.com/erlef/setup-beam/releases) - [Commits](erlef/setup-beam@2f0cc07...e6d7c94) Updates `actions/github-script` from 7.0.1 to 8.0.0 - [Release notes](https://github.com/actions/github-script/releases) - [Commits](actions/github-script@60a0d83...ed59741) Updates `webfactory/ssh-agent` from 0.9.0 to 0.9.1 - [Release notes](https://github.com/webfactory/ssh-agent/releases) - [Changelog](https://github.com/webfactory/ssh-agent/blob/master/CHANGELOG.md) - [Commits](webfactory/ssh-agent@dc588b6...a6f90b1) Updates `Swatinem/rust-cache` from ad397744b0d591a723ab90405b7247fac0e6b8db to 779680da715d629ac1d338a641029a2f4372abb5 - [Release notes](https://github.com/swatinem/rust-cache/releases) - [Changelog](https://github.com/Swatinem/rust-cache/blob/master/CHANGELOG.md) - [Commits](Swatinem/rust-cache@ad39774...779680d) Updates `ossf/scorecard-action` from 2.4.0 to 2.4.3 - [Release notes](https://github.com/ossf/scorecard-action/releases) - [Commits](ossf/scorecard-action@v2.4.0...v2.4.3) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: 6.0.2 dependency-type: direct:production update-type: version-update:semver-major dependency-group: actions - dependency-name: haskell-actions/setup dependency-version: 2.10.3 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: actions - dependency-name: actions/cache dependency-version: 5.0.3 dependency-type: direct:production update-type: version-update:semver-major dependency-group: actions - dependency-name: actions/upload-pages-artifact dependency-version: 4.0.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: actions - dependency-name: github/codeql-action dependency-version: 4.32.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: actions - dependency-name: erlef/setup-beam dependency-version: 1.20.4 dependency-type: direct:production update-type: version-update:semver-minor dependency-group: actions - dependency-name: actions/github-script dependency-version: 8.0.0 dependency-type: direct:production update-type: version-update:semver-major dependency-group: actions - dependency-name: webfactory/ssh-agent dependency-version: 0.9.1 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: actions - dependency-name: Swatinem/rust-cache dependency-version: 779680da715d629ac1d338a641029a2f4372abb5 dependency-type: direct:production dependency-group: actions - dependency-name: ossf/scorecard-action dependency-version: 2.4.3 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: actions ... Signed-off-by: dependabot[bot] <support@github.com>
dependabot
Bot
added
dependencies
Contributor
Author
|
Looks like these dependencies are updatable in another way, so this is no longer needed. |
dependabot
Bot
deleted the
dependabot/github_actions/actions-8062fc2ec2
branch
hyperpolymath
added a commit
that referenced
this pull request
Apr 12, 2026
posix_errors.v had two structural bugs:
1. Decision procedures declared as Axiom AFTER safe_* definitions that used them
(forward-reference error in Coq's sequential processing).
2. safe_* definitions used `negb (sumbool_val)` which is a type error —
negb : bool -> bool, but the sumbool {P} + {~P} is not a bool.
Fix:
- Moved decision procedures to BEFORE safe_* definitions.
- Proved path_exists_dec, is_directory_dec, is_file_dec,
has_write_permission_dec, path_eq_dec constructively by case-splitting on
the Filesystem function (Path -> option FSNode) and the FSNode fields.
- Kept is_empty_dir_dec as Axiom with full justification: universal
quantification over an infinite-domain function cannot be decided
constructively; finite-map refactor removes this axiom.
- Restructured safe_* definitions to use nested `if` on sumbool (correct)
instead of `negb (sumbool_val)` (type error). All existing theorems and
proofs preserved with minimal changes.
filesystem_composition.v: added detailed proof-strategy comments to
well_formed_ancestor_exists and mkdir_preserves_well_formed axioms,
referencing PROOF_HOLES_AUDIT.md items #1 and #2.
functional_extensionality: already correctly imported in filesystem_model.v;
all other files get it transitively via Require Import filesystem_model.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Apr 12, 2026
…ignore Convert well_formed_ancestor_exists and mkdir_preserves_well_formed from Axiom to Lemma via strong induction on path length. Add 6 helper lemmas: path_prefix_refl, path_prefix_length, path_prefix_eq_of_same_length, path_prefix_app_invert, parent_path_lt, path_prefix_parent — building the scaffolding described in PROOF_HOLES_AUDIT.md. Fix path_prefix bool type: `path_prefix p child` (Prop mis-use) → `path_prefix p child = true` throughout filesystem_model.v, posix_errors.v, and filesystem_composition.v. Fix rmdir_removes_path and mkdir_rmdir_reversible tactic sequences for Coq 8.20. Switch _CoqProject from -Q to -R (recursive logical path mapping). Add proofs/coq/.gitignore to exclude *.vo, *.vos, *.vok, *.glob, *.aux, Makefile, Makefile.conf from version control. Proof debt items #1 and #2 from docs/PROOF_HOLES_AUDIT.md are now CLOSED. Coq layer: 0 Admitted, 1 justified Axiom (is_empty_dir_dec — infinite-domain function, requires finite-map Filesystem refactor to eliminate). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Apr 12, 2026
Record 2026-04-12 session: 0 Admitted, 1 justified Axiom in Coq layer. Both deferred axioms (well_formed_ancestor_exists, mkdir_preserves_well_formed) proved and committed in 1ef841c. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Apr 27, 2026
posix_errors.v had two structural bugs:
1. Decision procedures declared as Axiom AFTER safe_* definitions that used them
(forward-reference error in Coq's sequential processing).
2. safe_* definitions used `negb (sumbool_val)` which is a type error —
negb : bool -> bool, but the sumbool {P} + {~P} is not a bool.
Fix:
- Moved decision procedures to BEFORE safe_* definitions.
- Proved path_exists_dec, is_directory_dec, is_file_dec,
has_write_permission_dec, path_eq_dec constructively by case-splitting on
the Filesystem function (Path -> option FSNode) and the FSNode fields.
- Kept is_empty_dir_dec as Axiom with full justification: universal
quantification over an infinite-domain function cannot be decided
constructively; finite-map refactor removes this axiom.
- Restructured safe_* definitions to use nested `if` on sumbool (correct)
instead of `negb (sumbool_val)` (type error). All existing theorems and
proofs preserved with minimal changes.
filesystem_composition.v: added detailed proof-strategy comments to
well_formed_ancestor_exists and mkdir_preserves_well_formed axioms,
referencing PROOF_HOLES_AUDIT.md items #1 and #2.
functional_extensionality: already correctly imported in filesystem_model.v;
all other files get it transitively via Require Import filesystem_model.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Apr 27, 2026
…ignore Convert well_formed_ancestor_exists and mkdir_preserves_well_formed from Axiom to Lemma via strong induction on path length. Add 6 helper lemmas: path_prefix_refl, path_prefix_length, path_prefix_eq_of_same_length, path_prefix_app_invert, parent_path_lt, path_prefix_parent — building the scaffolding described in PROOF_HOLES_AUDIT.md. Fix path_prefix bool type: `path_prefix p child` (Prop mis-use) → `path_prefix p child = true` throughout filesystem_model.v, posix_errors.v, and filesystem_composition.v. Fix rmdir_removes_path and mkdir_rmdir_reversible tactic sequences for Coq 8.20. Switch _CoqProject from -Q to -R (recursive logical path mapping). Add proofs/coq/.gitignore to exclude *.vo, *.vos, *.vok, *.glob, *.aux, Makefile, Makefile.conf from version control. Proof debt items #1 and #2 from docs/PROOF_HOLES_AUDIT.md are now CLOSED. Coq layer: 0 Admitted, 1 justified Axiom (is_empty_dir_dec — infinite-domain function, requires finite-map Filesystem refactor to eliminate). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Apr 27, 2026
Record 2026-04-12 session: 0 Admitted, 1 justified Axiom in Coq layer. Both deferred axioms (well_formed_ancestor_exists, mkdir_preserves_well_formed) proved and committed in c359aed. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Bumps the actions group with 10 updates in the / directory:
4.1.16.0.22.7.52.10.34.0.25.0.33.0.14.0.03.27.04.32.01.17.51.20.47.0.18.0.00.9.00.9.1ad397744b0d591a723ab90405b7247fac0e6b8db779680da715d629ac1d338a641029a2f4372abb52.4.02.4.3Updates
actions/checkoutfrom 4.1.1 to 6.0.2Release notes
Sourced from actions/checkout's releases.
... (truncated)
Commits
de0fac2Fix tag handling: preserve annotations and explicit fetch-tags (#2356)064fe7fAdd orchestration_id to git user-agent when ACTIONS_ORCHESTRATION_ID is set (...8e8c483Clarify v6 README (#2328)033fa0dAdd worktree support for persist-credentials includeIf (#2327)c2d88d3Update all references from v5 and v4 to v6 (#2314)1af3b93update readme/changelog for v6 (#2311)71cf226v6-beta (#2298)069c695Persist creds to a separate file (#2286)ff7abcdUpdate README to include Node.js 24 support details and requirements (#2248)08c6903Prepare v5.0.0 release (#2238)Updates
haskell-actions/setupfrom 2.7.5 to 2.10.3Release notes
Sourced from haskell-actions/setup's releases.
... (truncated)
Commits
f9150cbAdd Stack 3.9.1dc63c94Remove GHCup vanilla channel from defaults7786314await addGhcupReleaseChannel5757174Move all ghcup-add-channel commands into same groupca45ec3Remove broken GHC 9.12.3eb29c23Use GHCup vanilla and prereleases channels by default243ff44Add GHCs 9.14.1 and 9.12.3 and Cabal 3.16.1.00512451Fix #130: support GHCup on 32bit architecture (#131)45e5652Bump actions/checkout from 5 to 60a703b5Test: drop macos-13 (deprecated, does not support node 24)Updates
actions/cachefrom 4.0.2 to 5.0.3Release notes
Sourced from actions/cache's releases.
... (truncated)
Changelog
Sourced from actions/cache's changelog.
... (truncated)
Commits
cdf6c1fMerge pull request #1695 from actions/Link-/prepare-5.0.3a1bee22Add review for the@actions/http-clientlicense4695763Add licensed outputdc73bb9Upgrade dependencies and address security warnings345d5c2Add 5.0.3 builds8b402f5Merge pull request #1692 from GhadimiR/main304ab5alicense for httpclient609fc19Update licensed record for cacheb22231eBuild93150cdAdd PR link to releasesUpdates
actions/upload-pages-artifactfrom 3.0.1 to 4.0.0Release notes
Sourced from actions/upload-pages-artifact's releases.
Commits
7b1f4a7Merge pull request #127 from heavymachinery/pin-sha4cc19c7Pinactions/upload-artifactto SHA2d163beMerge pull request #107 from KittyChiu/mainc704843fix: linted README9605915Merge pull request #106 from KittyChiu/kittychiu/update-readme-1e59cdfeUpdate README.mda2d6704doc: updated usage section in readme984864eMerge pull request #105 from actions/Jcambass-patch-145dc788Add workflow file for publishing releases to immutable action packageefaad07Merge pull request #102 from actions/hidden-filesUpdates
github/codeql-actionfrom 3.27.0 to 4.32.0Release notes
Sourced from github/codeql-action's releases.
... (truncated)
Commits
b20883bMerge pull request #3428 from github/update-v4.32.0-e3b8227a2c9aa45dUpdate changelog for v4.32.0e3b8227Merge pull request #3427 from github/henrymercer/bump-for-new-minor-series8a01181Compare minor version number80e1425Bump minor version for CLI v2.24.0b748848Bump the Action minor version number on new CodeQL minor version series5e767efMerge pull request #3425 from github/update-bundle/codeql-bundle-v2.24.09752869Add changelog notec62c214Update default bundle to codeql-bundle-v2.24.025a224bMerge pull request #3423 from github/mbg/ci/yq-windowsUpdates
erlef/setup-beamfrom 1.17.5 to 1.20.4Release notes
Sourced from erlef/setup-beam's releases.
... (truncated)
Commits
e6d7c94Automation: update setup-beam version output to fceaea9fceaea9Fix: more versioning aroundnightlyandmaint/main(#359)2bb5b65Automation: update setup-beam version output to 1d4efdd1d4efddBump globals from 16.2.0 to 16.3.0 (#361)73f047eAutomation: update setup-beam version output to 6dd8a1a6dd8a1aBump@eslint/jsfrom 9.30.0 to 9.30.1 (#360)fd9a2e1Automation: update setup-beam version output to 65085e365085e3Bump eslint from 9.30.0 to 9.30.1 (#362)80c1659Automation: update setup-beam version output to 8e7fdef8e7fdefAutomation: update setup-beam version output to 1fe9179Updates
actions/github-scriptfrom 7.0.1 to 8.0.0Release notes
Sourced from actions/github-script's releases.
Commits
ed59741Merge pull request #653 from actions/sneha-krip/readme-for-v82dc352eBold minimum Actions Runner version in README01e118cUpdate README for Node 24 runtime requirements8b222acApply suggestion from@salmanmkcadc0eeaREADME for updating actions/github-script from v7 to v820fe497Merge pull request #637 from actions/node24e7b7f22update licenses2c81ba0Update Node.js version support to 24.xf28e40cMerge pull request #610 from actions/nebuk89-patch-11ae9958Update README.mdUpdates
webfactory/ssh-agentfrom 0.9.0 to 0.9.1Release notes
Sourced from webfactory/ssh-agent's releases.
Changelog
Sourced from webfactory/ssh-agent's changelog.
... (truncated)
Commits
a6f90b1Release v0.9.172c0bfdImprove documentation on why we use os.userInfo()e3f1a8eAcknowledge custom command inputs in cleanup.js (#235)b504c19Update CHANGELOG.mdUpdates
Swatinem/rust-cachefrom ad397744b0d591a723ab90405b7247fac0e6b8db to 779680da715d629ac1d338a641029a2f4372abb5Changelog
Sourced from Swatinem/rust-cache's changelog.
... (truncated)
Commits
Updates
ossf/scorecard-actionfrom 2.4.0 to 2.4.3Release notes
Sourced from ossf/scorecard-action's releases.
Commits
4eaacf0bump docker to ghcr v2.4.3 (#1587)42e3a01🌱 Bump the github-actions group with 3 updates (#1585)88c07ac🌱 Bump github.com/sigstore/cosign/v2 from 2.5.2 to 2.6.0 (#1579)6c690f2Bump github.com/ossf/scorecard/v5 from v5.2.1 to v5.3.0 (#1586)92083b5📖 Fix recommended command to test the image in development (#1583)7975ea6🌱 Bump the docker-images group across 1 directory with 2 updates (#1...0d1a743🌱 Bump github.com/spf13/cobra from 1.9.1 to 1.10.1 (#1575)46e6e0c🌱 Bump the github-actions group with 2 updates (#1580)c3f1350🌱 Improve printing options (#1584)43e475b🌱 Bump golang.org/x/net from 0.42.0 to 0.44.0 (#1578...Description has been truncated