ci: add lint check to prevent new panic! introductions

[tautschnig]

Add a CI lint step that flags any new panic! usage introduced by a PR. The check diffs against the PR's base branch, so pre-existing uses are not flagged. Individual lines can be suppressed with '-- nopanic:ok'.

• .github/scripts/checkNoPanic.sh: diff-based panic! detection script
• .github/workflows/ci.yml: added step to lint_checks job, with
  fetch-depth: 0 for merge-base resolution

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

Adds a CI lint to prevent introducing new panic! calls in Lean code by diffing only newly-added lines against the PR base.

Changes:

• Add .github/scripts/checkNoPanic.sh to detect newly introduced panic! in added .lean lines (with per-line suppression via -- nopanic:ok).
• Update lint_checks in .github/workflows/ci.yml to run the new script and fetch full git history for merge-base resolution.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
.github/workflows/ci.yml	Adds a lint step to run the new “no new panic!” check and configures full-depth checkout.
.github/scripts/checkNoPanic.sh	Implements diff-based detection of newly-added panic! occurrences in .lean files.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[MikaelMayer]

Although this PR adds one panic!, it's not in a lean file so not blocking the PR as expected. I would have loved to see one intermediate commit introducing such a panic to prove CI checks will fail, since it's the only way I imagine we can test this

[tautschnig]

Although this PR adds one panic!, it's not in a lean file so not blocking the PR as expected. I would have loved to see one intermediate commit introducing such a panic to prove CI checks will fail, since it's the only way I imagine we can test this

I had kiro-cli test this locally in the way you suggested, which worked out ok. Beyond that it might be up to us to spot if ever there is a PR that slips in a panic! yet that goes unnoticed by CI.

[atomb]

Although this PR adds one panic!, it's not in a lean file so not blocking the PR as expected. I would have loved to see one intermediate commit introducing such a panic to prove CI checks will fail, since it's the only way I imagine we can test this

I had kiro-cli test this locally in the way you suggested, which worked out ok. Beyond that it might be up to us to spot if ever there is a PR that slips in a panic! yet that goes unnoticed by CI.

I can easily imagine having a PR soon that temporarily includes a panic! that we expect to remove before merging. That would allow testing this. I'm okay with leaving a conclusive test until then.

[atomb]

Love the use of awk ;)

I suspect that, say, a Python script for this might be more readable and maintainable in the long run, but this looks correct and does the job.