fix(ci): align Lean action preflight with estate allowlist

[hyperpolymath]

GNPL and Lithoglyph fail Allowlist Preflight because the preflight list omits leanprover/lean-action, although config/settings/actions-allowlist.json already permits it. Add the same action to the preflight list so the two policy sources agree.

The authoritative scripts/check-allowed-actions.sh reproduced one Lean-action gap in each project before this change and reports zero gaps afterward (18 GNPL references and 26 Lithoglyph references). JSON parsing and patch whitespace checks pass. The projects retain their existing action lockfile validation and pinned Lean version.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 8fa9422d-a6a8-40a1-ab3f-f052544f0ad2

📥 Commits

Reviewing files that changed from the base of the PR and between 7f89241 and 486dda6.

📒 Files selected for processing (1)

• .machine_readable/REGISTRY.a2ml

Included review availability: Your plan provides up to 1 included review per hour; 0 remain after this review.

📜 Recent review details

⏰ Context from checks skipped due to timeout. (2)

• GitHub Check: scan / Hypatia Neurosymbolic Analysis
• GitHub Check: Repo self-tests

⚠️ CI failures not shown inline (6)

GitHub Actions: Secret Scanner / 0_scan _ gitleaks.txt: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run set -euo pipefail
 �[36;1mset -euo pipefail�[0m
 �[36;1m�[0m
 �[36;1m# fetch-depth: 0 on the checkout is load-bearing HERE. If it ever�[0m
 �[36;1m# regresses to the default depth-1 clone, detect would walk a single�[0m
 �[36;1m# commit, find nothing and report a pass — a gate that cannot fail.�[0m
 �[36;1m# Assert completeness from git itself: gitleaks' own "scanned N�[0m
 �[36;1m# commits" line under-reports and is not proof of depth.�[0m
 �[36;1mif [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then�[0m
 �[36;1m  echo "::error::checkout is shallow -- a history scan here would be vacuous; refusing to report a pass"�[0m

---

GitHub Actions: Secret Scanner / scan _ gitleaks: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run set -euo pipefail
 �[36;1mset -euo pipefail�[0m
 �[36;1m�[0m
 �[36;1m# fetch-depth: 0 on the checkout is load-bearing HERE. If it ever�[0m
 �[36;1m# regresses to the default depth-1 clone, detect would walk a single�[0m
 �[36;1m# commit, find nothing and report a pass — a gate that cannot fail.�[0m
 �[36;1m# Assert completeness from git itself: gitleaks' own "scanned N�[0m
 �[36;1m# commits" line under-reports and is not proof of depth.�[0m
 �[36;1mif [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then�[0m
 �[36;1m  echo "::error::checkout is shallow -- a history scan here would be vacuous; refusing to report a pass"�[0m

---

GitHub Actions: Secret Scanner / 1_scan _ shell-secrets.txt: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run # Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.
 �[36;1m# Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.�[0m
 �[36;1m# Restricted to *_TOKEN / *_KEY / *_SECRET / PASSWORD to keep false-positives low.�[0m
 �[36;1mPATTERNS=(�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*TOKEN[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*API_KEY[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*SECRET[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{16,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?***"'"'"'][^"'"'"']{6,}["'"'"']'�[0m
 �[36;1m)�[0m
 �[36;1m�[0m
 �[36;1m# Inline pragma patterns — suppress a hit when found on the same or�[0m
 �[36;1m# immediately preceding line.�[0m
 �[36;1mPRAGMA_RE='(scanner-allow:[[:space:]]*shell-secrets|hypatia:[[:space:]]*allow[[:space:]]+security_errors/secret_detected)'�[0m
 �[36;1m�[0m
 �[36;1m# Param-expansion RHS pattern — assignments whose value is a variable�[0m
 �[36;1m# reference rather than a literal are never real secrets.�[0m
 �[36;1m# Matches: ="$VAR"  ="${VAR}"  ="${VAR:-…}"  ="${VAR:?…}"  ='${VAR}'  =$VAR�[0m
 �[36;1mPARAM_EXPANSION_RE='=['"'"'"'"'"']?\$\{?[A-Za-z_][A-Za-z0-9_]*(:[?-][^}]*)?\}?['"'"'"'"'"']?[[:space:]]*(#.*)?$'�[0m
 �[36;1m�[0m
 �[36;1m# Load per-repo ignore globs from .shell-secrets-ignore if present.�[0m
 �[36;1mIGNORE_GLOBS=()�[0m
 �[36;1mif [[ -f .shell-secrets-ignore ]]; then�[0m
 �[36;1m  while IFS= read -r line || [[ -n "$line" ]]; do�[0m
 �[36;1m    # Skip blank lines and comments�[0m
 �[36;1m    [[ -z "$line" || "$line" == \#* ]] && continue�[0m
 �[36;1m    IGNORE_GLOBS+=("$line")�[0m
 �[36;1m  done < .shell-secrets-ignore�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m# is_ignored <filepath> — returns 0 (true) if path matches any ignore glob.�[0m
 �[36;1mis_ignored() {�[0m
 �[36;1m  local path="$1"�[0m
 �[36;1m  for glob in "${IGNORE_GLOBS[@]}"; do�[0m
 �[36;1m    #...

---

GitHub Actions: Secret Scanner / scan _ shell-secrets: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run # Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.
 �[36;1m# Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.�[0m
 �[36;1m# Restricted to *_TOKEN / *_KEY / *_SECRET / PASSWORD to keep false-positives low.�[0m
 �[36;1mPATTERNS=(�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*TOKEN[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*API_KEY[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*SECRET[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{16,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?***"'"'"'][^"'"'"']{6,}["'"'"']'�[0m
 �[36;1m)�[0m
 �[36;1m�[0m
 �[36;1m# Inline pragma patterns — suppress a hit when found on the same or�[0m
 �[36;1m# immediately preceding line.�[0m
 �[36;1mPRAGMA_RE='(scanner-allow:[[:space:]]*shell-secrets|hypatia:[[:space:]]*allow[[:space:]]+security_errors/secret_detected)'�[0m
 �[36;1m�[0m
 �[36;1m# Param-expansion RHS pattern — assignments whose value is a variable�[0m
 �[36;1m# reference rather than a literal are never real secrets.�[0m
 �[36;1m# Matches: ="$VAR"  ="${VAR}"  ="${VAR:-…}"  ="${VAR:?…}"  ='${VAR}'  =$VAR�[0m
 �[36;1mPARAM_EXPANSION_RE='=['"'"'"'"'"']?\$\{?[A-Za-z_][A-Za-z0-9_]*(:[?-][^}]*)?\}?['"'"'"'"'"']?[[:space:]]*(#.*)?$'�[0m
 �[36;1m�[0m
 �[36;1m# Load per-repo ignore globs from .shell-secrets-ignore if present.�[0m
 �[36;1mIGNORE_GLOBS=()�[0m
 �[36;1mif [[ -f .shell-secrets-ignore ]]; then�[0m
 �[36;1m  while IFS= read -r line || [[ -n "$line" ]]; do�[0m
 �[36;1m    # Skip blank lines and comments�[0m
 �[36;1m    [[ -z "$line" || "$line" == \#* ]] && continue�[0m
 �[36;1m    IGNORE_GLOBS+=("$line")�[0m
 �[36;1m  done < .shell-secrets-ignore�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m# is_ignored <filepath> — returns 0 (true) if path matches any ignore glob.�[0m
 �[36;1mis_ignored() {�[0m
 �[36;1m  local path="$1"�[0m
 �[36;1m  for glob in "${IGNORE_GLOBS[@]}"; do�[0m
 �[36;1m    #...

---

GitHub Actions: Secret Scanner / 2_scan _ rust-secrets.txt: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"
 �[36;1mTODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"�[0m
 �[36;1m�[0m
 �[36;1m# An unparseable cutoff would pick the warn branch forever, silently�[0m
 �[36;1m# disarming the widened scan. Refuse to run instead.�[0m
 �[36;1mrequire_date() {�[0m
 �[36;1m  case "$2" in�[0m
 �[36;1m    [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;;�[0m
 �[36;1m    *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD."�[0m

---

GitHub Actions: Secret Scanner / scan _ rust-secrets: fix(ci): align Lean action preflight with estate allowlist

Conclusion: failure

View job details

##[group]Run TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"
 �[36;1mTODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"�[0m
 �[36;1m�[0m
 �[36;1m# An unparseable cutoff would pick the warn branch forever, silently�[0m
 �[36;1m# disarming the widened scan. Refuse to run instead.�[0m
 �[36;1mrequire_date() {�[0m
 �[36;1m  case "$2" in�[0m
 �[36;1m    [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;;�[0m
 �[36;1m    *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD."�[0m

🔇 Additional comments (1)

.machine_readable/REGISTRY.a2ml (1)

210-210: LGTM!

---

📝 Summary

Summary by CodeRabbit

• Chores
  • Added leanprover/lean-action to the list of permitted GitHub Actions.

Walkthrough

The GitHub Actions allowlist now permits leanprover/lean-action at any version. The registry source hash reflects the updated tracked files.

Changes

Action allowlist

Layer / File(s)	Summary
Allow Lean Prover action rhodium-standard-repositories/actions-allowlist/allowed-actions.json, .machine_readable/REGISTRY.a2ml	Adds leanprover/lean-action@* to patterns_allowed and updates the corresponding source_hash.

Priority: ⬇️ Low

Estimated code review effort: 1 (Trivial) | ~2 minutes

Merge Risk: ⚪ Minimal · up to 486dd

This permits the Lean Prover GitHub Action and updates its registry metadata. The allowlist gap is resolved and no current merge-blocking risk remains.

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description check	✅ Passed	The description clearly explains that the pull request adds leanprover/lean-action to the CI preflight allowlist and resolves the reported gaps.
Title check	✅ Passed	The title clearly identifies the CI allowlist alignment for the Lean action, which matches the main change.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0…
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches 💡 1

🛠️ Fix failing CI checks 💡

• Create stacked PR
• Commit on current branch

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{A rabbit checked the action gate
Lean Prover may now pass its state
The registry hash aligns
With freshly tracked design
Small changes keep the build on time}

_{Comment @coderabbitai help to get the list of available commands.}

[coderabbitai]

✅ Coding Agent task started: View task and status

The task will inspect the CI failures, validate its fix, and open a stacked fix pull request automatically.

Note: Fixing CI failures is a beta feature and may encounter errors. Expect some limitations and changes as we gather feedback and continue to improve it.

[coderabbitai]

Rate Limit Exceeded

@hyperpolymath have exceeded the limit for the number of chat messages per hour. Please wait 35 minutes and 17 seconds before sending another message.

[sonarqubecloud]

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