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