feat: add nanoda external type checker support #145
Conversation
This PR adds support for verifying Lean projects with nanoda, an independent Lean 4 type checker written in Rust. New inputs: - `nanoda`: Enable nanoda verification (default: false) - `nanoda-allow-sorry`: Permit sorryAx axiom (default: true) - `nanoda-on-main-only`: Only run on push to main, not PRs (default: true) New output: - `nanoda-status`: SUCCESS | FAILURE | "" Also adds a reusable workflow `nanoda-daily.yml` for scheduled daily verification with configurable notifications (GitHub issue, webhook, or Zulip). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
austinletson
left a comment
austinletson
left a comment
There was a problem hiding this comment.
Looks good to me other than a few quesetions.
Love checking MathLib in 17 minutes on a GitHub runner!
| Allowed values: "true" | "false". | ||
| required: false | ||
| default: "true" | ||
| nanoda-on-main-only: |
There was a problem hiding this comment.
Would it make sense to encourage users to control the behavior through workflow events instead of having the nanoda-on-main-only. This would be more explicit and idiomatic. The users could either specify the events in the on block or with something like this:
- uses: leanprover/lean-action@v1
with:
nanoda: ${{ github.event_name == 'push' }}
I understand the convenience of nanoda-on-main-only for the standard single-job workflow. And it also would mean that it is backwards compatible with the existing single job workflow that comes with lake new, but I think this might cause confusion, especially looking at the usage in the nanoda-daily.yml workflow in this PR.
|
|
||
| # Step 2: Clone and build lean4export | ||
| echo "Cloning and building lean4export..." | ||
| # TODO: Once https://github.com/leanprover/lean4export/pull/11 is merged, |
There was a problem hiding this comment.
Since this is now merged can we resolve this TODO?
| CONFIG_FILE="_nanoda_config.json" | ||
|
|
||
| # Build permitted_axioms array | ||
| PERMITTED_AXIOMS='["propext", "Classical.choice", "Quot.sound", "Lean.trustCompiler"' |
There was a problem hiding this comment.
Why is Lean.trustCompiler included here by default? Isn't it and native_decide not allowed in Mathlib?
2 participants
This PR adds support for verifying Lean projects with nanoda, an independent Lean 4 type checker written in Rust.
New Inputs
nanoda"false"nanoda-allow-sorry"true"nanoda-on-main-only"true"New Output
nanoda-status:"SUCCESS"|"FAILURE"|""Reusable Daily Workflow
Also adds
.github/workflows/nanoda-daily.yml- a reusable workflow for scheduled daily verification with configurable notifications:Implementation Notes
kim-em/lean4exportfork with fix for nonDep normalization (pending fix: normalize nonDep flag for letE expressions lean4export#11)ammkrn/nanoda_libdebug branch with kernel compatibility fixesTesting
Successfully tested on:
🤖 Prepared with Claude Code