feat: use the bundled nanoda, and deprecate the nanoda input

.github/functional_tests/nanoda_bundled/action.yml

@@ -0,0 +1,56 @@
+name: 'nanoda bundled binaries test'
+description: 'Verify `nanoda: true` succeeds using the leanexport and nanoda_bin bundled with a recent toolchain, without building either from source.'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test. Must bundle `leanexport` and `nanoda_bin`.'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create a clean lake library
+      run: |
+        lake init foo lib
+        lake update
+      shell: bash
+
+    # `elan` sets the default toolchain without downloading it, so this can only run once
+    # something has actually used it: `lake update` above is the first thing that does.
+    - name: confirm the toolchain really does bundle both binaries
+      run: |
+        elan which leanexport
+        elan which nanoda_bin
+      shell: bash
+
+    - name: "run `lean-action` with `nanoda: true`"
+      id: lean-action-nanoda
+      uses: ./
+      with:
+        use-github-cache: false
+        nanoda: true
+
+    - name: verify nanoda accepted the clean package
+      env:
+        OUTPUT_NAME: "nanoda-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action-nanoda.outputs.nanoda-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    # The point of the change is that no Rust toolchain and no source builds are needed when the
+    # toolchain ships the binaries, so assert the source-build path did not run.
+    - name: verify nothing was built from source
+      run: |
+        if [ -d _lean4export ] || [ -d _nanoda_lib ]; then
+          echo "::error::the source-build fallback ran even though the toolchain bundles leanexport and nanoda_bin"
+          exit 1
+        fi
+        echo "no source builds, as expected"
+      shell: bash

.github/workflows/functional_tests.yml

@@ -28,6 +28,9 @@ env:
   # Toolchain without the bundled `leanchecker` binary,
   # used to cover the external `lean4checker` fallback path
   legacy_toolchain: leanprover/lean4:v4.26.0
+  # Bundles `leanexport` and `nanoda_bin`, which the `nanoda` step now prefers over building
+  # lean4export and nanoda_lib from source.
+  bundled_nanoda_toolchain: leanprover/lean4:v4.35.0-rc2
   # `lake check --paranoid` landed in v4.35.0-rc2, which is newer than the toolchain pinned in
   # `.github/functional_test_toolchain`, so the `lake-check` test pins its own.
   lake_check_toolchain: leanprover/lean4:v4.35.0-rc2
@@ -246,6 +249,14 @@ jobs:
           # axiom-audit builds with the project's toolchain, so use a recent one.
           toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
+  nanoda-bundled:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: ./.github/functional_tests/nanoda_bundled
+        with:
+          toolchain: ${{ env.bundled_nanoda_toolchain }}
+
   # `lake check` sandboxes with bubblewrap, which GitHub-hosted runners do not permit without a
   # privileged change to the runner. Namespace serves a privileged container, which permits it
   # outright, so that is where this runs. The `-with-features` suffix is what makes the feature

CHANGELOG.md

@@ -12,6 +12,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - new `lake-check` input to check the project with `lake check`: build it and replay the result through one or more kernels inside a sandbox, erroring on any use of a non-standard axiom. `"true"` uses Lean's own kernel; `"paranoid"` additionally runs every external checker the toolchain bundles (`leanchecker-paranoid`, `lean4lean`, `nanoda`, `con-leche` and `con-ron`), none of which has to be built. Requires a Linux runner, Lean `v4.35.0-rc1` or newer (`"paranoid"` needs `v4.35.0-rc2`), and a runner permitting the user namespaces bubblewrap needs; see the README. Default: false
 - new `lake-check-status` output parameter
 
+### Changed
+
+- `nanoda` now uses the `leanexport` and `nanoda_bin` bundled with the toolchain when it ships them, instead of installing a Rust toolchain and building lean4export and nanoda_lib from source on every run. Older toolchains keep the source-build path, and the axioms permitted are unchanged either way
+
+### Fixed
+
+- detect the module to export for `nanoda` from `defaultTargets` or the first `lean_lib`, rather than only from a `[package]` section. A current `lake init` writes no `[package]` section, so `nanoda: true` failed outright with "Could not detect module name"
+
+### Deprecated
+
+- `nanoda` and `nanoda-allow-sorry`, in favour of `lake-check: paranoid`. Note that `lake check` permits only the standard axioms, so there is no equivalent of `nanoda-allow-sorry: true`; projects carrying a `sorry` should stay on `nanoda` for now
+
 ## v1.6.1 - 2026-10-02
 
 ### Changed

README.md

@@ -238,9 +238,12 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Default: "false"
     lake-check: ""
 
+    # Deprecated: use `lake-check: paranoid`, except when `nanoda-allow-sorry: true` is
+    # needed; `lake check` permits only the standard axioms and cannot tolerate a `sorry`.
     # 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).
+    # Uses the `leanexport` and `nanoda_bin` bundled with the toolchain when available,
+    # otherwise builds lean4export and nanoda_lib from source (installing Rust if needed).
     # Allowed values: "true" | "false".
     # Default: "false"
     nanoda: ""

action.yml

@@ -133,9 +133,15 @@ inputs:
     default: "false"
   nanoda:
     description: |
+      Deprecated: use `lake-check: paranoid`, which runs nanoda among every other checker
+      bundled with the toolchain. There is no migration for `nanoda-allow-sorry: true`, because
+      `lake check` permits only the standard axioms, so a project that needs `sorry` tolerated
+      should stay on this input for now.
       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).
+      Uses the `leanexport` and `nanoda_bin` bundled with the toolchain when it ships them,
+      and otherwise builds lean4export and nanoda_lib from source, which needs a Rust toolchain
+      (installed automatically if not present).
       Allowed values: "true" | "false".
     required: false
     default: "false"

scripts/run_nanoda.sh

@@ -5,6 +5,8 @@ set -e
 echo "::group::nanoda Output"
 echo "Checking environment with nanoda external type checker"
 
+echo "::warning::\`nanoda\` is deprecated; use \`lake-check: paranoid\` instead, which runs nanoda together with every other checker bundled with the toolchain. It has no equivalent of \`nanoda-allow-sorry: true\`, because \`lake check\` permits only the standard axioms, so projects that carry a \`sorry\` should stay on this input for now."
+
 # handle_exit function to capture exit status and cleanup
 handle_exit() {
     exit_status=$?
@@ -32,47 +34,77 @@ if [ -d "_lean4export" ] || [ -d "_nanoda_lib" ]; then
     exit 1
 fi
 
-# Step 1: Install Rust if not present
-echo "Checking for Rust installation..."
-if ! command -v cargo &> /dev/null; then
-    echo "Installing Rust toolchain..."
-    curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal
-    # shellcheck source=/dev/null
-    source "$HOME/.cargo/env"
+# Recent release toolchains ship both the exporter and nanoda, matched to each other and to the
+# compiler that produced the oleans. When they are there, use them: cloning and building
+# `lean4export` and `nanoda_lib` costs a Rust toolchain and two source builds on every run, and
+# pins `nanoda_lib` to a branch rather than a release.
+BUNDLED_EXPORTER="$(elan which leanexport 2>/dev/null || true)"
+BUNDLED_NANODA="$(elan which nanoda_bin 2>/dev/null || true)"
+
+if [ -n "$BUNDLED_EXPORTER" ] && [ -x "$BUNDLED_EXPORTER" ] \
+    && [ -n "$BUNDLED_NANODA" ] && [ -x "$BUNDLED_NANODA" ]; then
+    echo "Using the leanexport and nanoda_bin bundled with this toolchain"
+    EXPORTER="$BUNDLED_EXPORTER"
+    NANODA="$BUNDLED_NANODA"
 else
-    echo "Rust already installed: $(cargo --version)"
-fi
+    echo "This toolchain bundles no nanoda; building it and lean4export from source"
+
+    # Step 1: Install Rust if not present
+    echo "Checking for Rust installation..."
+    if ! command -v cargo &> /dev/null; then
+        echo "Installing Rust toolchain..."
+        curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile minimal
+        # shellcheck source=/dev/null
+        source "$HOME/.cargo/env"
+    else
+        echo "Rust already installed: $(cargo --version)"
+    fi
+
+    # Step 2: Clone and build lean4export
+    echo "Cloning and building lean4export..."
+    git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export
 
-# Step 2: Clone and build lean4export
-echo "Cloning and building lean4export..."
-git clone --depth 1 https://github.com/leanprover/lean4export.git _lean4export
+    # Copy lean-toolchain to lean4export so it uses matching Lean version
+    cp lean-toolchain _lean4export/
 
-# Copy lean-toolchain to lean4export so it uses matching Lean version
-cp lean-toolchain _lean4export/
+    (
+        cd _lean4export
+        lake build
+    )
 
-(
-    cd _lean4export
-    lake build
-)
+    # Step 3: Clone and build nanoda_lib
+    echo "Cloning and building nanoda_lib..."
+    # Using debug branch which has fixes for recent Lean kernel changes
+    git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nanoda_lib
 
-# Step 3: Clone and build nanoda_lib
-echo "Cloning and building nanoda_lib..."
-# Using debug branch which has fixes for recent Lean kernel changes
-git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nanoda_lib
+    (
+        cd _nanoda_lib
+        cargo build --release
+    )
 
-(
-    cd _nanoda_lib
-    cargo build --release
-)
+    EXPORTER="_lean4export/.lake/build/bin/lean4export"
+    NANODA="_nanoda_lib/target/release/nanoda_bin"
+fi
 
 # Step 4: Detect module name from lakefile
 echo "Detecting module name..."
 MODULE_NAME=""
 
-# Try lakefile.toml first
+# Try lakefile.toml first. Prefer `defaultTargets`, then the first `lean_lib`: those name the
+# module to export, where the package name need not be a module at all. `lake init foo lib` on a
+# current toolchain writes `name = "foo"` at the top level with no `[package]` section and a
+# library called `Foo`, so looking only for a package name finds nothing to export.
 if [ -f "lakefile.toml" ]; then
-    # Extract name from [package] section
-    MODULE_NAME=$(grep -A5 '^\[package\]' lakefile.toml | grep '^name' | head -1 | sed 's/.*= *"\([^"]*\)".*/\1/' || true)
+    MODULE_NAME=$(grep -m1 '^defaultTargets' lakefile.toml | sed -n 's/.*\[[^"]*"\([^"]*\)".*/\1/p' || true)
+
+    if [ -z "$MODULE_NAME" ]; then
+        MODULE_NAME=$(grep -A3 '^\[\[lean_lib\]\]' lakefile.toml | grep -m1 '^name' | sed 's/.*= *"\([^"]*\)".*/\1/' || true)
+    fi
+
+    # Older lakefiles put the package name in a `[package]` section.
+    if [ -z "$MODULE_NAME" ]; then
+        MODULE_NAME=$(grep -A5 '^\[package\]' lakefile.toml | grep '^name' | head -1 | sed 's/.*= *"\([^"]*\)".*/\1/' || true)
+    fi
 fi
 
 # Fallback to lakefile.lean
@@ -91,7 +123,7 @@ echo "Detected module name: $MODULE_NAME"
 # Step 5: Export the project
 echo "Exporting $MODULE_NAME..."
 EXPORT_FILE="_nanoda_export.txt"
-lake env _lean4export/.lake/build/bin/lean4export "$MODULE_NAME" > "$EXPORT_FILE"
+lake env "$EXPORTER" "$MODULE_NAME" > "$EXPORT_FILE"
 
 echo "Export file size: $(wc -c < "$EXPORT_FILE") bytes"
 echo "Export file lines: $(wc -l < "$EXPORT_FILE") lines"
@@ -126,6 +158,6 @@ cat "$CONFIG_FILE"
 # Step 7: Run nanoda
 echo ""
 echo "Running nanoda type checker..."
-_nanoda_lib/target/release/nanoda_bin "$CONFIG_FILE"
+"$NANODA" "$CONFIG_FILE"
 
 echo "nanoda check completed successfully"