build(deps): bump the actions group with 7 updates - #1
Closed
dependabot[bot] wants to merge 1 commit into
Closed
Conversation
Bumps the actions group with 7 updates: | Package | From | To | | --- | --- | --- | | [actions/checkout](https://github.com/actions/checkout) | `4.1.1` | `6.0.1` | | [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.2` | | [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.31.10` | | [webfactory/ssh-agent](https://github.com/webfactory/ssh-agent) | `0.9.0` | `0.9.1` | | [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.1 - [Release notes](https://github.com/actions/checkout/releases) - [Commits](actions/checkout@v4.1.1...v6.0.1) 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.2 - [Release notes](https://github.com/actions/cache/releases) - [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md) - [Commits](actions/cache@0c45773...8b402f5) 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.31.10 - [Release notes](https://github.com/github/codeql-action/releases) - [Commits](github/codeql-action@v3.27.0...v4.31.10) 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 `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.1 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.2 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.31.10 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: 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>
dependabotBotforce-pushed
the
dependabot/github_actions/actions-690794c5dc
branch
from
January 22, 2026 21:08
e98a559 to
70c600bCompareContributorAuthor
Looks like these dependencies are updatable in another way, so this is no longer needed. |
dependabotBot
deleted the
dependabot/github_actions/actions-690794c5dc
branch
January 29, 2026 15:51
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 was referenced Jun 1, 2026
hyperpolymath added a commit
that referenced
this pull request
Jun 1, 2026
…hPerms variant (#67) Closes the long-standing [admit.] in [single_op_reversible] (OpRmdir and OpDeleteFile branches) by taking closure path #2 from the documented design note: the [Operation] inductive now carries [OpMkdirWithPerms : Path -> Permissions -> Operation] and [OpCreateFileWithPerms : Path -> Permissions -> Operation] constructors, and [reverse_op] is threaded with the pre-state so the inverse of [OpRmdir]/[OpDeleteFile] can capture the original node's permissions exactly. Changes: * filesystem_composition.v - Operation: +2 constructors (OpMkdirWithPerms, OpCreateFileWithPerms). - mkdir_with / create_file_with: write a node at a path with the supplied permissions (instead of default_perms). - apply_op: handle the two new constructors. - reverse_op: now [Operation -> Filesystem -> Operation]; for OpRmdir/OpDeleteFile, look up the node and route to the ...WithPerms variant. - reverse_sequence: now stateful; LIFO threading of pre-states. - reverse_sequence_app / _singleton: re-proved under the new signature. - op_precondition / reversible: extended to the new constructors. - single_op_reversible: now closed with Qed (no admits). All 6 cases discharged from [reversible op fs] alone. - operation_sequence_reversible / two_op_ / three_op_ / reversible_creates_CNO: re-stated under the new reverse_sequence threading; proofs adjusted. - Print Assumptions at end-of-file: 3 lines, each showing only [functional_extensionality_dep] — the same axiom already used by [mkdir_rmdir_reversible] in the base model. No new axioms. * filesystem_equivalence.v - apply_op_preserves_equiv: +2 branches for the new constructors. - mkdir_with_preserves_equiv / create_file_with_preserves_equiv: added (same shape as their default-perms cousins). - reversible_creates_equiv / sequence_reversible_equiv / cno_identity_element / sequence_cno_identity: re-stated under the threaded [reverse_op]/[reverse_sequence] signatures. Out of scope (pre-existing admit unchanged): - [mkdir_two_dirs_reversible] is still [Admitted.] — it documents a non-LIFO sequence-reversal that is independent of the model-gap closed here. Refs #41 (Phase 1) Refs #42 (proof inventory) Closure path #2 ("OpMkdirWithPerms variant") chosen — the directive called this the cleanest. Path #1 would have required strengthening [reversible] with a [fs p = Some (mkFSNode _ default_perms)] side condition; path #3 (UndoLog) is heavier-weight. Echo-types audit: not relevant — this is L1 (region-mode) shape, not L3 (echo). Recorded per [feedback_proofs_must_check_and_cross_doc_echo_types]. Local build oracle (mandatory per [feedback_proof_pr_build_oracle_is_only_truth]): coq_makefile -f _CoqProject -o build.mk && make -f build.mk GREEN on Coq 8.18.0. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Merged
5 tasks
hyperpolymath added a commit
that referenced
this pull request
Jun 1, 2026
…factor + 15-25 prop-tests (#72) - secure_delete (commands::secure_deletion::secure_delete) lifted to a public, documented primitive: 3-pass overwrite (urandom / zeros / 0xFF) with fsync between passes + unlink. Uses /dev/urandom on Unix, falls back to a hash-mixed PRNG elsewhere. CoW / FTL / snapshot limitations documented at the module-level rustdoc. - audit_log: added AuditLog::default_path() and AuditLog::with_default_path() honouring XDG_STATE_HOME / $HOME per the XDG Base Directory spec (XDG_STATE_HOME/valence-shell/audit.log or $HOME/.local/state/valence-shell/audit.log). - Replaced all six `unreachable!()` calls in src/commands.rs with typed `CommandError` (`#[non_exhaustive]`) variants — InternalUnreachableInverseArm, InternalUnreachableIrreversible, InternalUnreachableExplainPathArm — plus a contextual anyhow::bail! for the &str-returning hardware-erase dispatch. Future regressions in upstream filtering now surface as recoverable errors rather than aborting the shell. - Added impl/rust-cli/tests/secure_audit_prop_tests.rs with 20 property tests covering: - mkdir/rmdir reversibility (Lean: FilesystemModel.mkdir_rmdir_reversible) - touch/rm reversibility - writeFileReversible - copyFile_reversible - obliterate_not_injective (no inverse exists) - inverse round-trip well-formedness for all reversible OperationTypes - secure_delete unlink behaviour + EISDIR + ENOENT + edge sizes (0, 1) - audit-log append-only / order-preservation / filter-by-type - audit-entry JSON round-trip - XDG default-path resolution - Implemented the two security_tests.rs stubs (security_gdpr_secure_deletion, security_audit_trail_immutability) which previously held TODO markers. Echo-types audit: filesystem-reversibility properties exercised here are L3 (echo-layer) shape per the prior estate sweep. The implementation does not yet *import* echo-types directly — recorded as relevant-but-not-yet-imported per the cross-doc directive. Local verification: - cargo build --lib : clean - cargo test --workspace : 757 passed / 0 failed (the 21 test-binaries all return "0 failed", including the new 20 prop-tests and the 2 unstubbed security_tests). - cargo clippy --workspace --tests : pre-existing absurd_extreme_comparisons errors in confirmation.rs and e2e_script_execution.rs persist (verified against main via stash). Zero new clippy warnings on changed files. Closes the practice-gap #1 + #2 from #45. Refs #41 Phase 1, #43 prop-test expansion. Co-authored-by: Claude Opus 4.7 (1M context) <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 freeto 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 7 updates:
4.1.16.0.12.7.52.10.34.0.25.0.23.0.14.0.03.27.04.31.100.9.00.9.12.4.02.4.3Updates
actions/checkoutfrom 4.1.1 to 6.0.1Release notes
Sourced from actions/checkout's releases.
... (truncated)
Commits
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)9f26565Update actions checkout to use node 24 (#2226)08eba0bPrepare release v4.3.0 (#2237)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.2Release notes
Sourced from actions/cache's releases.
... (truncated)
Changelog
Sourced from actions/cache's changelog.
... (truncated)
Commits
8b402f5Merge pull request #1692 from GhadimiR/main304ab5alicense for httpclient609fc19Update licensed record for cacheb22231eBuild93150cdAdd PR link to releases9b8ca9fBump actions/cache to 5.0.39255dc7Merge pull request #1686 from actions/cache-v5.0.1-release8ff5423chore: release v5.0.19233019Merge pull request #1685 from salmanmkc/node24-storage-blob-fixb975f2bfix: add peer property to package-lock.json for dependenciesUpdates
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.31.10Release notes
Sourced from github/codeql-action's releases.
... (truncated)
Commits
cdefb33Merge pull request #3394 from github/update-v4.31.10-0fa411efdcfa77c6Update changelog for v4.31.100fa411eMerge pull request #3393 from github/update-bundle/codeql-bundle-v2.23.9c284324Add changelog note83e7d00Update default bundle to codeql-bundle-v2.23.9f6a16beMerge pull request #3391 from github/dependabot/npm_and_yarn/npm-minor-f1cdf5...c1f5f1aRebuild1805d8dBump the npm-minor group with 2 updatesb2951d2Merge pull request #3353 from github/kaspersv/bump-min-cli-v-for-overlay41448d9Merge pull request #3287 from github/henrymercer/generate-mergeback-lastUpdates
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
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)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 rebasewill rebase this PR@dependabot recreatewill recreate this PR, overwriting any edits that have been made to it@dependabot mergewill merge this PR after your CI passes on it@dependabot squash and mergewill squash and merge this PR after your CI passes on it@dependabot cancel mergewill cancel a previously requested merge and block automerging@dependabot reopenwill reopen this PR if it is closed@dependabot closewill close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually@dependabot show <dependency name> ignore conditionswill show all of the ignore conditions of the specified dependency@dependabot ignore <dependency name> major versionwill 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 versionwill 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