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!

action.yml

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>

scripts/run_nanoda.sh

.github/workflows/nanoda-daily.yml

- 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>

- Always close log group (::endgroup::) on both success and failure - Check for pre-existing directories before cloning to prevent data loss - Fix misleading notifications when Zulip config is invalid but verification succeeded Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

cursor

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

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

cursor · 2026-01-26T23:59:01Z

scripts/run_nanoda.sh

+
+# Step 2: Clone and build lean4export
+echo "Cloning and building lean4export..."
+git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export


Wrong repository URL for lean4export

High Severity

The PR description states the implementation "Uses kim-em/lean4export fork with fix for nonDep normalization (pending leanprover/lean4export#11)", but the code clones from https://github.com/leanprover/lean4export.git instead. If the referenced fix hasn't been merged to the upstream repository, nanoda verification will fail on projects that depend on the nonDep normalization fix.

cursor · 2026-01-26T23:59:01Z

.github/workflows/nanoda-daily.yml

+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5
+        with:
+          api-key: ${{ secrets.zulip-api-key }}
+          email: 'github-bot@${{ inputs.zulip-org-url }}'


Hardcoded Zulip bot email prevents custom bot names

Medium Severity

The Zulip bot email is hardcoded as github-bot@${{ inputs.zulip-org-url }}, assuming all users have a bot named github-bot. Zulip bot email addresses depend on the name chosen during bot creation. Users with differently-named bots (e.g., ci-bot, notifications-bot) will experience authentication failures when attempting to use Zulip notifications.

Additional Locations (1)

.github/workflows/nanoda-daily.yml#L140-L141

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

scripts/run_nanoda.sh Show resolved Hide resolved

scripts/run_nanoda.sh Show resolved Hide resolved

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

kim-em and others added 2 commits January 25, 2026 16:42

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>

cursor bot reviewed Jan 26, 2026

View reviewed changes

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!

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!

Uh oh!

Uh oh!

Uh oh!

cursor bot left a comment

Uh oh!

cursor bot Jan 26, 2026

Uh oh!

cursor bot Jan 26, 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!

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!

Uh oh!

Uh oh!

Uh oh!

cursor bot left a comment

Choose a reason for hiding this comment

Uh oh!

cursor bot Jan 26, 2026

Choose a reason for hiding this comment

Wrong repository URL for lean4export

Uh oh!

cursor bot Jan 26, 2026

Choose a reason for hiding this comment

Hardcoded Zulip bot email prevents custom bot names

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants