feat: add nanoda to parallel workflow

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>

Author: kim-em

.github/workflows/ci.yml

@@ -91,6 +91,23 @@ on:
         type: string
         required: false
         default: "false"
+      nanoda:
+        description: |
+          Check environment with nanoda external type checker.
+          nanoda is an independent Lean 4 type checker written in Rust.
+          Requires Rust toolchain (will be installed automatically if not present).
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "false"
+      nanoda-allow-sorry:
+        description: |
+          When running nanoda, permit the sorryAx axiom.
+          Set to "false" if your project should have no sorry placeholders.
+          Allowed values: "true" | "false".
+        type: string
+        required: false
+        default: "true"
     outputs:
       build-status:
         description: "Status of lake build: SUCCESS | FAILURE | ''"
@@ -107,6 +124,9 @@ on:
       detected-mathlib:
         description: "Whether Mathlib dependency was detected"
         value: ${{ jobs.build.outputs.detected-mathlib }}
+      nanoda-status:
+        description: "Status of nanoda check: SUCCESS | FAILURE | ''"
+        value: ${{ jobs.nanoda.outputs.nanoda-status }}
 
 jobs:
   build:
@@ -312,3 +332,36 @@ jobs:
             "${{ github.event.repository.license.spdx_id }}"
         shell: bash
         working-directory: ${{ inputs.lake-package-directory }}
+
+  nanoda:
+    needs: build
+    if: inputs.nanoda == 'true'
+    runs-on: ubuntu-latest
+    outputs:
+      nanoda-status: ${{ steps.nanoda.outputs.nanoda-status }}
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: install elan
+        run: |
+          : Install Elan
+          "${GITHUB_WORKSPACE}/scripts/install_elan.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}
+
+      - uses: actions/cache/restore@v4
+        if: inputs.use-github-cache == 'true'
+        with:
+          path: ${{ inputs.lake-package-directory }}/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}
+
+      - name: nanoda
+        id: nanoda
+        env:
+          NANODA_ALLOW_SORRY: ${{ inputs.nanoda-allow-sorry }}
+        run: |
+          : Check Environment with nanoda
+          "${GITHUB_WORKSPACE}/scripts/run_nanoda.sh"
+        shell: bash
+        working-directory: ${{ inputs.lake-package-directory }}

CHANGELOG.md

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
+- new parallel reusable workflow `.github/workflows/ci.yml` that runs test, lint, leanchecker, nanoda, and reservoir checks in parallel
 - new `nanoda` input to check environment with [nanoda](https://github.com/ammkrn/nanoda_lib) external type checker
 - new `nanoda-allow-sorry` input to permit sorryAx axiom when running nanoda (default: true)
 - new `nanoda-status` output parameter

README.md

@@ -140,7 +140,7 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
 
 ## Parallel Workflow
 
-For faster CI, `lean-action` provides a reusable workflow that runs test, lint, lean4checker, and reservoir checks in parallel on separate runners:
+For faster CI, `lean-action` provides a reusable workflow that runs test, lint, lean4checker, nanoda, and reservoir checks in parallel on separate runners:
 
 ```yaml
 name: CI
@@ -158,14 +158,15 @@ jobs:
       test: "true"
       lint: "true"
       lean4checker: "true"
+      nanoda: "true"
 ```
 
 The parallel workflow:
 - Runs a **build** job first (elan setup, config, mathlib cache, lake build)
-- Then runs **test**, **lint**, **lean4checker**, and **reservoir** jobs in parallel
+- Then runs **test**, **lint**, **lean4checker**, **nanoda**, and **reservoir** jobs in parallel
 - Each parallel job restores the build cache from the build job
 
-All inputs from the standard action are supported. The workflow outputs the same status parameters (`build-status`, `test-status`, `lint-status`, `mk_all-status`).
+All inputs from the standard action are supported. The workflow outputs the same status parameters (`build-status`, `test-status`, `lint-status`, `mk_all-status`, `nanoda-status`).
 
 ## Customization