feat: add parallel workflow with nanoda support#146
Open
kim-em wants to merge 11 commits into
Open
Conversation
Add a new reusable workflow (.github/workflows/ci.yml) that runs test, lint, lean4checker, and reservoir checks in parallel on separate runners after the build job completes. - Build job: elan setup, config, mathlib cache, lake build - Parallel jobs: test, lint, lean4checker, reservoir - Each parallel job restores the build cache - Same inputs/outputs as the existing composite action - Existing action.yml preserved for backward compatibility 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
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>
Resolves TODO - leanprover/lean4export#11 was merged on 2026-01-07. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
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>
- 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>
- 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>
- 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>
Add nanoda external type checker as a parallel job in ci.yml workflow: - New inputs: nanoda, nanoda-allow-sorry - New output: nanoda-status - Runs in parallel with test, lint, lean4checker, and reservoir 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
kim-em
force-pushed
the
feat/parallel-with-nanoda
branch
from
9392248 to
1ef98a0
Compare
The parallel workflow was still referencing the deprecated `lean4checker` input and the old `run_lean4checker.sh` script name; since upstream renamed the script file the job would have failed at runtime.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Combines #144 and #145, and adds nanoda as a parallel job in the reusable workflow.
🤖 Prepared with Claude Code