Skip to content

Run external Nanoda checks in parallel - #88

Closed
luckyseoul wants to merge 1 commit into
leanprover:masterfrom
luckyseoul:codex/nanoda-parallel-workers
Closed

luckyseoul wants to merge 1 commit into
leanprover:masterfrom
luckyseoul:codex/nanoda-parallel-workers

Conversation

@luckyseoul

Copy link
Copy Markdown

Sets Nanoda's num_threads explicitly for external kernel checks. This changes scheduling only; declaration checks, strictness, and permitted-axiom policy are unchanged. Verified: lake build comparator lean4export and all 20 Comparator tests pass with Nanoda available.

@luckyseoul

Copy link
Copy Markdown
Author

Closing: this machine-specific worker count should not be upstreamed as a hard-coded default.

@luckyseoul luckyseoul closed this Sep 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant