Skip to content

docs(flake): annotate KEEP+DEP rationale (standards#102) - #13

Merged
hyperpolymath merged 1 commit into
mainfrom
keep-nix-mirror-101-devtools
May 19, 2026
Merged

hyperpolymath merged 1 commit into
mainfrom
keep-nix-mirror-101-devtools

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Refs standards#101 standards#102.

Per the Nix-mirror retirement campaign (Wave 5), echidnabot's flake is LOAD-BEARING (KEEP+DEP): the dev shell is the sole source of postgresql and the Rust dev-tool surface (cargo-edit, cargo-audit, cargo-outdated, cargo-tarpaulin, cargo-deny, cargo-watch, cargo-deb, cargo-generate-rpm, jq, sqlx-cli) — none of which are in the guix.scm manifest (pkg-config/rust/rust-cargo/sqlite/openssl + pinned crates) nor in the sealed Containerfile (rust:1.83 + pkg-config/libsqlite3-dev/sqlite-libs/ca-certificates).

This PR adds the rule-3 annotation so the flake's retention is self-documenting. No package-set change.

🤖 Generated with Claude Code

Per the campaign gate, this flake is LOAD-BEARING — sole source of
postgresql and the Rust dev-tool surface (cargo-edit/audit/outdated/
tarpaulin/deny/watch/deb/generate-rpm, jq, sqlx-cli) not in the
guix.scm manifest (pkg-config/rust/rust-cargo/sqlite/openssl +
pinned crates) nor in the sealed Containerfile (rust:1.83 + pkg-config/
libsqlite3-dev/sqlite-libs/ca-certificates).

Refs standards#101 standards#102.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
hyperpolymath merged commit bf2e748 into main May 19, 2026
13 of 17 checks passed
@github-actions

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 34 issues detected

Severity Count
🔴 Critical 11
🟠 High 7
🟡 Medium 16

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Stale AI task file -- delete or move to docs/",
    "type": "stale",
    "file": "SONNET-TASKS.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "echidnabot.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (2 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/echidnabot/echidnabot/proofs/coq/admitted_stub.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (1 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/echidnabot/echidnabot/proofs/coq/admitted_stub.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/echidnabot/echidnabot/src/abi/Foreign.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "sorry leaves proof hole (3 occurrences, CWE-704)",
    "type": "sorry",
    "file": "/home/runner/work/echidnabot/echidnabot/proofs/lean/sorry_stub.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
    "type": "lean_axiom",
    "file": "/home/runner/work/echidnabot/echidnabot/proofs/lean/sorry_stub.lean",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant