feat: add nanoda external type checker support #145

kim-em · 2026-01-06T04:34:24Z

This PR adds support for verifying Lean projects with nanoda, an independent Lean 4 type checker written in Rust.

New Inputs

Input	Default	Description
`nanoda`	`"false"`	Enable nanoda verification
`nanoda-allow-sorry`	`"true"`	Permit sorryAx axiom
`nanoda-on-main-only`	`"true"`	Only run on push to main, not PRs

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:

jobs:
  verify:
    uses: leanprover/lean-action/.github/workflows/nanoda-daily.yml@v1
    # Notifications: issue (default), webhook, zulip, or none

Implementation Notes

Rust toolchain is installed automatically if not present
Uses kim-em/lean4export fork with fix for nonDep normalization (pending fix: normalize nonDep flag for letE expressions lean4export#11)
Uses ammkrn/nanoda_lib debug branch with kernel compatibility fixes

Testing

Successfully tested on:

sphere-eversion: 352,154 declarations (~6 min)
Carleson: 353,613 declarations (~6 min)
FLT: 420,742 declarations (~11 min)
Mathlib: 627,356 declarations (~17 min)

🤖 Prepared with Claude Code

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 <noreply@anthropic.com>

austinletson

Looks good to me other than a few quesetions.

Love checking MathLib in 17 minutes on a GitHub runner!

austinletson · 2026-01-08T02:01:56Z

action.yml

+      Allowed values: "true" | "false".
+    required: false
+    default: "true"
+  nanoda-on-main-only:


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.

Good point! I've removed nanoda-on-main-only in 8865ac2. Users can now control when nanoda runs through workflow events:

nanoda: ${{ github.event_name == 'push' }}

This is more explicit and idiomatic.

scripts/run_nanoda.sh

austinletson · 2026-01-08T02:12:53Z

scripts/run_nanoda.sh

+CONFIG_FILE="_nanoda_config.json"
+
+# Build permitted_axioms array
+PERMITTED_AXIOMS='["propext", "Classical.choice", "Quot.sound", "Lean.trustCompiler"'


Why is Lean.trustCompiler included here by default? Isn't it and native_decide not allowed in Mathlib?

Lean.trustCompiler is required because Init includes Lean.reduceBool and Lean.reduceNat, which are opaque declarations that reference Lean.trustCompiler in their definitions. Even though they're opaque, their definitions are still type-checked, so any project importing Init will transitively depend on Lean.trustCompiler.

This does NOT allow native_decide proofs through - those use Lean.ofReduceBool or Lean.ofReduceNat, which are not in the permitted list. So nanoda would still catch any native_decide usage.

As Robin Arnez noted: "To Nanoda, Lean.trustCompiler is just an axiom that asserts that True is true" - it's harmless because nanoda doesn't support compiler evaluation anyway.

See the discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Why%20does%20the%20daily%20Nanoda%20check%20allow%20%60Lean.trustCompiler%60%3F

Resolves TODO - leanprover/lean4export#11 was merged on 2026-01-07. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Resolve CHANGELOG.md conflict - nanoda features go under Unreleased, v1.4.0 already released with test-args and elan fix. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

action.yml

scripts/run_nanoda.sh

Users should control nanoda execution through workflow events instead, which is more explicit and idiomatic. For example: nanoda: ${{ github.event_name == 'push' }} This avoids confusion and gives users full control over when nanoda runs. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

.github/workflows/nanoda-daily.yml

- Move cleanup into trap handler so temporary directories are removed even when nanoda verification fails (fixes re-run failures on self-hosted runners) - Add validation step for zulip-org-url and zulip-api-key inputs when notify is set to 'zulip', matching the webhook validation Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

.github/workflows/nanoda-daily.yml

- Add --fail to curl so HTTP errors are not silently ignored - Add always() to Zulip validation so it runs even when nanoda fails Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

cursor

Cursor Bugbot has reviewed your changes and found 3 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with Cloud Agents, enable Autofix in the Cursor dashboard.}

cursor · 2026-01-25T05:42:18Z

scripts/run_nanoda.sh

+
+    if [ $exit_status -ne 0 ]; then
+        echo "nanoda-status=FAILURE" >> "$GITHUB_OUTPUT"
+        echo "::error::nanoda check failed"


Log group left unclosed on failure path

Low Severity

The handle_exit function only calls ::endgroup:: in the success branch (line 21), not in the failure branch. When nanoda check fails, the log group opened at line 5 with ::group::nanoda Output is never closed, leaving the GitHub Actions log output with an unclosed group that makes logs harder to read during debugging.

cursor · 2026-01-25T05:42:18Z

scripts/run_nanoda.sh

+
+    # Always cleanup temporary files/directories
+    echo "Cleaning up temporary files..."
+    rm -rf _lean4export _nanoda_lib _nanoda_export.txt _nanoda_config.json


Cleanup deletes pre-existing user directories on failure

Medium Severity

If a user's project already contains directories named _lean4export or _nanoda_lib, the git clone at lines 40 and 53 will fail with "destination path already exists". Due to set -e, the script exits, triggering the trap handler which unconditionally runs rm -rf _lean4export _nanoda_lib .... This deletes the user's pre-existing directories, causing data loss. The script lacks a check for existing directories before cloning and doesn't track which resources it actually created.

Additional Locations (1)

scripts/run_nanoda.sh#L39-L40

cursor · 2026-01-25T05:42:18Z

.github/workflows/nanoda-daily.yml

+          if [ -z "$ZULIP_API_KEY" ]; then
+            echo "::error::zulip-api-key secret is required when notify is set to 'zulip'"
+            exit 1
+          fi


Zulip validation failure triggers wrong notification type

Medium Severity

When notify: 'zulip' is configured but Zulip credentials are missing, the validation step (line 107) runs with if: always() and fails. This causes failure() to return true for subsequent steps. If nanoda verification succeeded but Zulip validation failed, the "Send Zulip notification on failure" step (line 135) will attempt to run and send a misleading "verification failed" message, when actually the verification succeeded and only the notification config was invalid.

Additional Locations (1)

.github/workflows/nanoda-daily.yml#L133-L145

- Remove references to nanoda-on-main-only input from README (was removed in 8865ac2) - Allow leading whitespace when detecting package name in lakefile.lean Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

kim-em and others added 2 commits January 6, 2026 15:33

fix: remove secrets from step if conditions (actionlint)

4d15b16

kim-em mentioned this pull request Jan 6, 2026

feat: add parallel workflow with nanoda support #146

Open

austinletson approved these changes Jan 8, 2026

View reviewed changes

kim-em and others added 2 commits January 25, 2026 15:43

fix: use upstream lean4export now that PR leanprover#11 is merged

5609f14

Resolves TODO - leanprover/lean4export#11 was merged on 2026-01-07. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Merge branch 'main' into feat-nanoda

e900c07

Resolve CHANGELOG.md conflict - nanoda features go under Unreleased, v1.4.0 already released with test-args and elan fix. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

cursor bot reviewed Jan 25, 2026

View reviewed changes

action.yml Outdated Show resolved Hide resolved

scripts/run_nanoda.sh Outdated Show resolved Hide resolved

cursor bot reviewed Jan 25, 2026

View reviewed changes

.github/workflows/nanoda-daily.yml Show resolved Hide resolved

cursor bot reviewed Jan 25, 2026

View reviewed changes

.github/workflows/nanoda-daily.yml Show resolved Hide resolved

.github/workflows/nanoda-daily.yml Show resolved Hide resolved

fix: webhook --fail flag and zulip validation always()

4ff2a50

- Add --fail to curl so HTTP errors are not silently ignored - Add always() to Zulip validation so it runs even when nanoda fails Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

cursor bot reviewed Jan 25, 2026

View reviewed changes

fix: remove stale nanoda-on-main-only docs, improve module detection

56a79b8

- Remove references to nanoda-on-main-only input from README (was removed in 8865ac2) - Allow leading whitespace when detecting package name in lakefile.lean Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add nanoda external type checker support #145

feat: add nanoda external type checker support #145

kim-em commented Jan 6, 2026

Uh oh!

austinletson left a comment

Uh oh!

austinletson Jan 8, 2026

Uh oh!

kim-em Jan 25, 2026

Uh oh!

Uh oh!

austinletson Jan 8, 2026

Uh oh!

kim-em Jan 25, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cursor bot left a comment

Uh oh!

cursor bot Jan 25, 2026

Uh oh!

cursor bot Jan 25, 2026

Uh oh!

cursor bot Jan 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

feat: add nanoda external type checker support #145

Are you sure you want to change the base?

feat: add nanoda external type checker support #145

Conversation

kim-em commented Jan 6, 2026

New Inputs

New Output

Reusable Daily Workflow

Implementation Notes

Testing

Uh oh!

austinletson left a comment

Choose a reason for hiding this comment

Uh oh!

austinletson Jan 8, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em Jan 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

austinletson Jan 8, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em Jan 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cursor bot left a comment

Choose a reason for hiding this comment

Uh oh!

cursor bot Jan 25, 2026

Choose a reason for hiding this comment

Log group left unclosed on failure path

Uh oh!

cursor bot Jan 25, 2026

Choose a reason for hiding this comment

Cleanup deletes pre-existing user directories on failure

Uh oh!

cursor bot Jan 25, 2026

Choose a reason for hiding this comment

Zulip validation failure triggers wrong notification type

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants