fix: detect TOML lean_lib modules for nanoda

.github/functional_tests/nanoda_toml/action.yml

@@ -0,0 +1,37 @@
+name: "nanoda with a TOML Lake package"
+description: "Verify nanoda detects the package module from current lakefile.toml syntax"
+inputs:
+  toolchain:
+    description: "Lean toolchain used by the generated test package"
+    required: true
+runs:
+  using: composite
+  steps:
+    - 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 TOML Lake package
+      run: |
+        lake init nanodatoml .toml
+        lake update
+      shell: bash
+
+    - name: run lean-action with nanoda
+      id: lean-action
+      uses: ./
+      with:
+        nanoda: true
+        nanoda-allow-sorry: false
+        use-github-cache: false
+
+    - name: verify nanoda success
+      env:
+        OUTPUT_NAME: nanoda-status
+        EXPECTED_VALUE: SUCCESS
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.nanoda-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/workflows/functional_tests.yml

@@ -7,180 +7,226 @@ on:
       - "scripts/**"
       - "action.yml"
       - ".github/workflows/functional_tests.yml"
+      - ".github/functional_test_toolchain"
       - ".github/functional_tests/**"
   workflow_dispatch:
     inputs:
       toolchain:
-        description: "The Lean toolchain to use when running the tests."
+        description: "The Lean toolchain to use when running the tests. Defaults to the toolchain pinned in .github/functional_test_toolchain."
         required: false
-        default: "leanprover/lean4:v4.26.0"
+        default: ""
 
-# This environment variable is necessary in addition to the workflow_dispatch input
-# because the workflow_dispatch input is not available when the workflow is triggered by a pull request
 env:
-  toolchain: ${{ github.event.inputs.toolchain || 'leanprover/lean4:v4.26.0' }}
-  modern_toolchain: leanprover/lean4:v4.28.0
+  # Toolchain without the bundled `leanchecker` binary,
+  # used to cover the external `lean4checker` fallback path
+  legacy_toolchain: leanprover/lean4:v4.26.0
 
 jobs:
+  # The default toolchain is pinned in `.github/functional_test_toolchain`
+  # rather than in this file so that the `Update Functional Test Toolchain`
+  # workflow can bump it without a token holding the `workflows` permission,
+  # which the default `GITHUB_TOKEN` cannot be granted.
+  resolve-toolchain:
+    runs-on: ubuntu-latest
+    outputs:
+      toolchain: ${{ steps.resolve.outputs.toolchain }}
+    steps:
+      - uses: actions/checkout@v6
+      - name: Resolve the functional test toolchain
+        id: resolve
+        env:
+          # The workflow_dispatch input is unset when the workflow is triggered
+          # by a pull request, in which case the pinned toolchain is used.
+          input_toolchain: ${{ github.event.inputs.toolchain }}
+        run: |
+          toolchain="${input_toolchain:-$(tr -d '[:space:]' < .github/functional_test_toolchain)}"
+          if [ -z "$toolchain" ]; then
+            echo "::error::failed to resolve the functional test toolchain"
+            exit 1
+          fi
+          echo "Using toolchain: $toolchain"
+          echo "toolchain=$toolchain" >> "$GITHUB_OUTPUT"
+
   lake-init-success:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        # run `lean-action` on a package generated with `lake init` for:
-        #  - a standalone package
-        #  - a package with a mathlib dependency
-        #  - a package with a `lakefile.toml` file
-        # see ./github/functional_tests/lake_init/action.yml for more details on lake-init-arguments
         lake-init-arguments: ["standalone", "mathdep math", "tomltest .toml"]
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_init_success
         with:
           lake-init-arguments: ${{ matrix.lake-init-arguments}}
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-init-failure:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_init_failure
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   auto-config-true:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/auto_config_true
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   auto-config-false:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/auto_config_false
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
-  auto-config-false-modern-leanchecker:
+  auto-config-false-legacy-leanchecker:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v5
       - uses: ./.github/functional_tests/auto_config_false
         with:
-          toolchain: ${{ env.modern_toolchain }}
+          toolchain: ${{ env.legacy_toolchain }}
 
   lake-build-args:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_build_args
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-test-args:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_test_args
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   detect-mathlib:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/mathlib_dependency
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-test-success:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_test_success
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-test-failure:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_test_failure
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-lint-success:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_lint_success
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-lint-failure:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_lint_failure
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   lake-check-test-failure:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_check_test_failure
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   subdirectory-lake-package:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/subdirectory_lake_package
         with:
-          toolchain: ${{ env.toolchain }}
-  
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
+
   subdirectory-lake-package-lean-checker:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v5
       - uses: ./.github/functional_tests/subdirectory_lake_package_lean_checker
         with:
-          toolchain: ${{ env.modern_toolchain }}
+          toolchain: ${{ env.legacy_toolchain }}
 
   reinstall-transient-toolchain:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/reinstall-transient-toolchain
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   mk_all-check:
+    needs: resolve-toolchain
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/mk_all-check
         with:
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
+
+  nanoda-toml-package:
+    needs: resolve-toolchain
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: ./.github/functional_tests/nanoda_toml
+        with:
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   macos-runner:
+    needs: resolve-toolchain
     runs-on: macos-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_init_success
         with:
           lake-init-arguments: "standalone"
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
   windows-runner:
+    needs: resolve-toolchain
     runs-on: windows-latest
     steps:
-      - uses: actions/checkout@v5
+      - uses: actions/checkout@v6
       - uses: ./.github/functional_tests/lake_init_success
         with:
           lake-init-arguments: "standalone"
-          toolchain: ${{ env.toolchain }}
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}

CHANGELOG.md

@@ -7,6 +7,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Fixed
+
+- use a more portable shebang, useful for self-hosted runners
+- Fix nanoda module discovery for current Lake TOML packages by reading the
+  `lean_lib` name rather than assuming the package name is also a module.
+
 ## v1.5.0 - 2026-04-21
 
 ### Added

scripts/run_nanoda.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 set -e
 
 # Group logging using the ::group:: workflow command
@@ -71,8 +71,16 @@ MODULE_NAME=""
 
 # Try lakefile.toml first
 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)
+    # nanoda exports a Lean module, so prefer the first lean_lib name. This is
+    # distinct from the package name in current `lake init .toml` output.
+    MODULE_NAME=$(sed -n '/^[[:space:]]*\[\[lean_lib\]\][[:space:]]*$/,/^[[:space:]]*\[\[/p' lakefile.toml |
+        sed -n 's/^[[:space:]]*name[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' |
+        head -1 || true)
+    # Compatibility fallback for older files where package and module names
+    # coincide and no explicit lean_lib section is present.
+    if [ -z "$MODULE_NAME" ]; then
+        MODULE_NAME=$(sed -n 's/^[[:space:]]*name[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' lakefile.toml | head -1 || true)
+    fi
 fi
 
 # Fallback to lakefile.lean