fix: detect TOML lean_lib modules for nanoda

.github/functional_tests/nanoda_toml/action.yml

@@ -0,0 +1,50 @@
+name: "nanoda with a TOML Lake package"
+description: "Verify nanoda detects the lean_lib 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
+        echo "lakefile.toml:"
+        cat lakefile.toml
+      shell: bash
+
+    # Full nanoda SUCCESS is blocked by the debug-branch NDJSON parse error
+    # (#169 / #177). This job asserts the TOML discovery fix: lake init emits
+    # package `nanodatoml` and module `Nanodatoml`, and run_nanoda.sh must
+    # choose the lean_lib name.
+    - name: detect nanoda module from lakefile.toml
+      env:
+        NANODA_DETECT_ONLY: "true"
+        GITHUB_OUTPUT: ${{ runner.temp }}/nanoda-detect-output
+      run: |
+        set -euo pipefail
+        : > "$GITHUB_OUTPUT"
+        output="$(scripts/run_nanoda.sh)"
+        echo "$output"
+        package_name="$(sed -n 's/^[[:space:]]*name[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' lakefile.toml | head -1)"
+        if [ "$package_name" != "nanodatoml" ]; then
+          echo "::error::expected lake init package name nanodatoml, got ${package_name}"
+          exit 1
+        fi
+        if echo "$output" | grep -q "Detected module name: nanodatoml"; then
+          echo "::error::nanoda used the package name instead of the lean_lib module"
+          exit 1
+        fi
+        if ! echo "$output" | grep -q "Detected module name: Nanodatoml"; then
+          echo "::error::expected nanoda to detect lean_lib module Nanodatoml"
+          exit 1
+        fi
+      shell: bash

.github/workflows/functional_tests.yml

@@ -234,6 +234,15 @@ jobs:
           # axiom-audit builds with the project's toolchain, so use a recent one.
           toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
 
+  nanoda-toml-package:
+    needs: resolve-toolchain
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/functional_tests/nanoda_toml
+        with:
+          toolchain: ${{ needs.resolve-toolchain.outputs.toolchain }}
+
   macos-runner:
     needs: resolve-toolchain
     runs-on: macos-latest

CHANGELOG.md

@@ -23,6 +23,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - include `lake-package-directory` when hashing `lean-toolchain` and `lake-manifest.json` for the GitHub cache key, so projects whose Lake package lives in a subdirectory get a version-specific key instead of an empty one (the empty key previously caused stale, cross-version cache restores)
 - 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
 

scripts/run_nanoda.sh

@@ -16,12 +16,21 @@ handle_exit() {
     echo "Cleaning up temporary files..."
     rm -rf _lean4export _nanoda_lib _nanoda_export.txt _nanoda_config.json
 
-    if [ $exit_status -ne 0 ]; then
-        echo "nanoda-status=FAILURE" >> "$GITHUB_OUTPUT"
+    # Detection-only mode is used by the TOML fixture and does not run nanoda.
+    if [ "${NANODA_DETECT_ONLY:-}" = "true" ]; then
+        return
+    fi
+
+    if [ -n "${GITHUB_OUTPUT:-}" ]; then
+        if [ $exit_status -ne 0 ]; then
+            echo "nanoda-status=FAILURE" >> "$GITHUB_OUTPUT"
+            echo "::error::nanoda check failed"
+        else
+            echo "nanoda-status=SUCCESS" >> "$GITHUB_OUTPUT"
+            echo
+        fi
+    elif [ $exit_status -ne 0 ]; then
         echo "::error::nanoda check failed"
-    else
-        echo "nanoda-status=SUCCESS" >> "$GITHUB_OUTPUT"
-        echo
     fi
 }
 trap handle_exit EXIT
@@ -32,6 +41,46 @@ if [ -d "_lean4export" ] || [ -d "_nanoda_lib" ]; then
     exit 1
 fi
 
+# Detect module name from lakefile before installing nanoda. Current
+# `lake init name .toml` emits a package name distinct from the Lean module
+# root, so nanoda must export the first lean_lib name rather than the package.
+echo "Detecting module name..."
+MODULE_NAME=""
+
+# Try lakefile.toml first
+if [ -f "lakefile.toml" ]; then
+    # 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
+if [ -z "$MODULE_NAME" ] && [ -f "lakefile.lean" ]; then
+    # Try to extract from 'package' declaration (allowing leading whitespace)
+    MODULE_NAME=$(grep -E "^\s*package\s+" lakefile.lean | head -1 | awk '{print $2}' || true)
+fi
+
+if [ -z "$MODULE_NAME" ]; then
+    echo "::error::Could not detect module name from lakefile.toml or lakefile.lean"
+    exit 1
+fi
+
+echo "Detected module name: $MODULE_NAME"
+
+# The TOML fixture uses this to assert discovery without running nanoda, whose
+# debug-branch parser currently rejects lean4export NDJSON (#169 / #177).
+if [ "${NANODA_DETECT_ONLY:-}" = "true" ]; then
+    echo "Skipping nanoda export (NANODA_DETECT_ONLY=true)"
+    exit 0
+fi
+
 # Step 1: Install Rust if not present
 echo "Checking for Rust installation..."
 if ! command -v cargo &> /dev/null; then
@@ -65,38 +114,15 @@ git clone --depth 1 --branch debug https://github.com/ammkrn/nanoda_lib.git _nan
     cargo build --release
 )
 
-# Step 4: Detect module name from lakefile
-echo "Detecting module name..."
-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)
-fi
-
-# Fallback to lakefile.lean
-if [ -z "$MODULE_NAME" ] && [ -f "lakefile.lean" ]; then
-    # Try to extract from 'package' declaration (allowing leading whitespace)
-    MODULE_NAME=$(grep -E "^\s*package\s+" lakefile.lean | head -1 | awk '{print $2}' || true)
-fi
-
-if [ -z "$MODULE_NAME" ]; then
-    echo "::error::Could not detect module name from lakefile.toml or lakefile.lean"
-    exit 1
-fi
-
-echo "Detected module name: $MODULE_NAME"
-
-# Step 5: Export the project
+# Step 4: Export the project
 echo "Exporting $MODULE_NAME..."
 EXPORT_FILE="_nanoda_export.txt"
 lake env _lean4export/.lake/build/bin/lean4export "$MODULE_NAME" > "$EXPORT_FILE"
 
 echo "Export file size: $(wc -c < "$EXPORT_FILE") bytes"
 echo "Export file lines: $(wc -l < "$EXPORT_FILE") lines"
 
-# Step 6: Create nanoda config
+# Step 5: Create nanoda config
 echo "Creating nanoda configuration..."
 CONFIG_FILE="_nanoda_config.json"