ci: regenerate lockfile after dependabot bumps (restores CodeQL, Scorecard, Governance) - #158
Merged
Merged
Conversation
Dependabot bumped action SHAs without regenerating actions.lock, so 7 of 15 workflows went stale: CodeQL and OSSF Scorecard back to startup_failure, and the Governance linter's own 'gh actions-lock --verify-local' step failing on the same staleness. Regenerated with the full recipe — gh actions-lock, restore the inline SHA pins, relock-sha-keys.sh, then restore the reusable-caller entries the generator drops — and re-pinned the six standards wrappers to 08586a1. --verify-local: all 15 workflows covered; --no-fix: valid, zero errors. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This comment has been minimized.
This comment has been minimized.
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
hyperpolymath
added a commit
that referenced
this pull request
Aug 7, 2026
… register (#159) The code is in good shape; the prose describing it was not. This pass makes the documentation true, and catalogues what it can't fix in one place. Everything below was **verified against the tree**, not assumed — including re-running the test suite (**221 pass, 0 failures** — the README's long-published number reproduces exactly). ## Licence safety (highest priority) `PALIMPSEST.adoc` asserted *"This project is licensed under the Palimpsest-MPL License 1.0"*, contradicting `LICENSE` (MPL-2.0). The repo migrated off PMPL on **2026-05-26** per estate audit `standards#196` — so this was a leftover creating genuine licensing ambiguity. Rewritten as a clearly-marked historical note. Six further licence inconsistencies are catalogued but **not** unilaterally fixed, because they need your decision — notably `dialects/solo/compiler/Cargo.toml` declaring `license = "MIT OR Palimpsest-0.8"` (**not a valid SPDX identifier**) and two `LICENSE` files whose SPDX tag says MPL-2.0 while their body is Palimpsest text copyrighted to a different party. ## Structural `CONTRIBUTING.md` was **broken**: it opened mid-code-block (so line 7 rendered as an H1 "# Clone the repository"), ended unterminated, carried two conflicting SPDX identifiers, and described a "Perimeter 1-3" layout that doesn't exist here. Rewritten against the real 15-crate workspace — including the actual signing requirement (the `main` ruleset enforces `required_signatures`; the `.adoc` twin claimed DCO sign-off) and a section on proof-affecting changes. ## Factual corrections | Was | Is | |---|---| | `ROADMAP.adoc`: *"Initial development phase"*, every box unchecked, *"to be determined based on community feedback"* | Real rung state for a 0.2.0 tree with a working LLVM pipeline — plus an explicit **Not planned** section | | `README.adoc`: 137 tests, F1.0, four co-equal dialects, proof CI "future" | Short accurate pointer to `README.md` (it contradicted it on every load-bearing number) | | `EXPLAINME.adoc`: *".hypatia-baseline.json is an intentionally empty array"* | It has **7 entries expiring 2026-10-27** (#145) | | Wiki ×3: *"preservation in progress"* / *"statement-only, gated on #93"* | Machine-checked, axiom-free, CI-gated since F1.4; #93 resolved | ## Honesty banners, not deletions 11 wiki pages document behaviour that doesn't exist — an installer at `mylang.org`, Homebrew/apt packages, an `ml` binary (it's `my`), a retracted `std::` module tree, `async`/`await`, live AI queries. Rather than delete ~13k lines unilaterally, each now carries a warning banner naming the specific debt item. A reader can no longer be misled; you can still decide what to keep. ## Machine-readable - `STATE.a2ml`: head commit `8636e15`→`e68bb3d`; the "FULLY GREEN" board claim corrected; the *"Idris `?todo_preservation` deliberately open"* note contradicted both `proofs/STATUS.md` and the tree (zero holes remain). - **Notable**: `STATE.a2ml` listed S3c.3-choice as `pending` while `proofs.yml:319` already gates it axiom-free — the proof work was ahead of its own records. - `ECOSYSTEM.a2ml` (two months stale): gaps G1/G2/G3/G5 all closed; "four dialects" retracted to the nested-subset model. ## New: `DEBT.md` **34 items** across licence · documentation · code · proof · test · CI/CD · metadata — 8 high, 21 medium, 5 low. Each records *the command that produced its evidence*, so items can be re-measured rather than re-argued. Unverified items are labelled **DIAGNOSIS (unconfirmed)** rather than asserted. Highlights beyond the licence issues: - **C-1** ~7,300 LOC of orphaned duplicate source in root `src/`+`lib/` — unbuilt, divergent, and documented by the wiki *as if it were the compiler* - **P-1** `proofs.yml` triggers only on `proofs/verification/**`, so changing the *checker* never re-runs the proof gate — exactly the change most likely to break the spec↔implementation correspondence - **P-2** the Idris job has no hole assertion (a typed hole type-checks), so it would pass if one were reintroduced - **T-1** 34 property tests in `tests/property_tests.rs` are wired to no target and never compile - **I-1** actions-lockfile regeneration is a recurring manual step after every dependabot bump (this bit us today — see #158) ## Wiki + repo metadata The GitHub wiki was a **29-byte stub** while 26 pages sat unpublished. It's now five pages (Home, Getting-Started, Architecture, Formal-Verification, Project-Status) plus a sidebar — deliberately a *navigational* layer linking to in-repo docs so it can't drift. Live and rendering. Description and topics replaced. The old topics (`development`, `hyperpolymath`, `open-source`, `rust`, `software`, `tooling`) either named you or duplicated GitHub's own language detection. The new nine are concept-level and chosen for discoverability: `quantitative-type-theory`, `affine-types`, `linear-types`, `mechanized-metatheory`, `session-types`, `verified-compiler`, `programming-language-design`, `proof-engineering`, `type-systems`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Aug 7, 2026
…rtup-failing (#160) OSSF Scorecard has been dying daily with a 0-second `startup_failure`, and it **outlasted the lockfile repair in #158** — so it is a second, distinct cause. ## Cause A job-level `permissions:` block **replaces** the workflow-level one; it does not merge with it. `scorecard.yml` grants `actions: read` at workflow level, but the job that calls the reusable re-declared only `contents` / `security-events` / `id-token` — dropping `actions: read` exactly where it is needed. The standards `scorecard-reusable.yml` requests `actions: read` at line 9, and **a reusable asking for more than its caller grants is rejected before any job is created**. That is why there was never a log, an annotation, or a check run to look at. This matches the estate-wide reusable-permission-escalation pattern. ## Verification Canary dispatch on this branch (run 31175237558): **1 job ran** where previously there were **0**. The startup rejection is gone. That job then fails with `Only the default branch main is supported` — which is the Scorecard action refusing to run on a non-default branch, i.e. **an artefact of canarying on a branch, not a defect**. It will run properly once this is on `main`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <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
1 participant
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.
Dependabot bumps #155 and #157 changed action SHAs without regenerating
.github/workflows/actions.lock— the churn flagged when the lockfile first landed. Result on main: 7 of 15 workflows stale, CodeQL and OSSF Scorecard back to 0-secondstartup_failure, and the Governance job red because its owngh actions-lock --verify-localstep (standards #574) correctly detected the staleness.Full recipe applied:
gh actions-lockregeneratesha_pinning_requiredstays ON)relock-sha-keys.shto re-key the lockfile to those SHAsuses:union08586a1Verification:
--verify-local→ All 15 workflows have complete lockfile coverage;--no-fix→ valid, zero errors.relock-caller-entries.shto standards so the estate has the whole recipe in one place.🤖 Generated with Claude Code