Skip to content

fix(ci): ungate lean-offline from push/schedule - #194

Merged
fraware merged 1 commit into
mainfrom
fix/wave7-lean-offline-no-midsave
Jul 16, 2026
Merged

fix(ci): ungate lean-offline from push/schedule#194
fraware merged 1 commit into
mainfrom
fix/wave7-lean-offline-no-midsave

Conversation

@fraware

@fraware fraware commented Jul 16, 2026

Copy link
Copy Markdown
Member

Summary

  • Tip lean-offline still wedged runners during/after mathlib vendor (verify hung 20m after successful cache save; vendor exceeded 40m with no step kill)
  • Make lean-offline workflow_dispatch-only so inventory is not gated on an unachievable cold-cache path; lean-morph remains push-gated Lean CI
  • Add concurrency, drop mid-job cache/save, fold verify into vendor

Test plan

  • After merge, inventory no longer lists lean-offline as gated red
  • proof-bot remains green on tip
  • Manual lean-offline dispatch still available

GitHub-hosted runners hang during/after mathlib vendor (step timeouts
stop firing). Push-gated Lean stays on lean-morph; lean-offline becomes
workflow_dispatch-only with concurrency, no mid-job cache save, and
verify folded into the vendor step.
@cursor

cursor Bot commented Jul 16, 2026

Copy link
Copy Markdown

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

@github-actions

Copy link
Copy Markdown

Thanks for the PR! CI will run CERT validation and replay checks. Results will appear in workflow badges and artifacts.

@fraware
fraware merged commit 8a83949 into main Jul 16, 2026
23 of 25 checks passed
@fraware
fraware deleted the fix/wave7-lean-offline-no-midsave branch July 16, 2026 11:36
@github-actions

Copy link
Copy Markdown

SBOM Security Report

Total Packages: 4536

Language Distribution:

  • go: 359
  • javascript: 3277
  • rust: 592
  • python: 1

License Distribution:

  • MIT: 1270
  • Apache-2.0: 45
  • CC0-1.0: 43
  • BSD-3-Clause: 34
  • ISC: 87
  • BSD-2-Clause: 41
  • Python-2.0: 2
  • MPL-2.0: 1
  • Unlicense: 5
  • CC-BY-4.0: 1
  • (Apache-2.0 OR MPL-1.1): 1
  • BlueOak-1.0.0: 3
  • (AFL-2.1 OR BSD-3-Clause): 2
  • (BSD-3-Clause OR GPL-2.0): 1
  • 0BSD: 3
  • (MIT OR CC0-1.0): 4
  • MIT AND ISC: 1

✅ SBOM generated successfully
✅ No GPL licenses detected
✅ No high/critical vulnerabilities found

fraware added a commit that referenced this pull request Jul 16, 2026
Unblock ci-honesty after #194 left an unjustified `|| true` on iptables
restore. Closest scoped fix so ART ungate PR can pass required CI.
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