From 1a27fef4b556c0e0d6d8c1699036ad820b055889 Mon Sep 17 00:00:00 2001 From: Sean Collins <173011278+SMC17@users.noreply.github.com> Date: Thu, 20 Aug 2026 14:50:33 -0400 Subject: [PATCH 1/2] fix: detect TOML lean_lib modules for nanoda Prefer the first [[lean_lib]] name when exporting for nanoda. Current `lake init name .toml` emits a package name distinct from the Lean module root, so searching only for a legacy [package] section fails. --- .../functional_tests/nanoda_toml/action.yml | 37 +++++++++++++++++++ .github/workflows/functional_tests.yml | 9 +++++ CHANGELOG.md | 2 + scripts/run_nanoda.sh | 12 +++++- 4 files changed, 58 insertions(+), 2 deletions(-) create mode 100644 .github/functional_tests/nanoda_toml/action.yml diff --git a/.github/functional_tests/nanoda_toml/action.yml b/.github/functional_tests/nanoda_toml/action.yml new file mode 100644 index 0000000..3364afb --- /dev/null +++ b/.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 diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml index 367f88a..0f683b4 100644 --- a/.github/workflows/functional_tests.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f80944..455307c 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/scripts/run_nanoda.sh b/scripts/run_nanoda.sh index 6675345..5cc56b0 100755 --- a/scripts/run_nanoda.sh +++ b/scripts/run_nanoda.sh @@ -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 From 3af6bf2df6b21eb94947a6637b1f580d9679c874 Mon Sep 17 00:00:00 2001 From: Sean Collins <173011278+SMC17@users.noreply.github.com> Date: Thu, 20 Aug 2026 15:10:43 -0400 Subject: [PATCH 2/2] test: assert nanoda TOML lean_lib detection without full nanoda SUCCESS Full nanoda SUCCESS is blocked by #169 (debug-branch NDJSON parse). The fixture now runs run_nanoda.sh in detect-only mode against `lake init name .toml` and requires the lean_lib module name. --- .../functional_tests/nanoda_toml/action.yml | 43 ++++++--- scripts/run_nanoda.sh | 94 +++++++++++-------- 2 files changed, 84 insertions(+), 53 deletions(-) diff --git a/.github/functional_tests/nanoda_toml/action.yml b/.github/functional_tests/nanoda_toml/action.yml index 3364afb..22541cf 100644 --- a/.github/functional_tests/nanoda_toml/action.yml +++ b/.github/functional_tests/nanoda_toml/action.yml @@ -1,5 +1,5 @@ name: "nanoda with a TOML Lake package" -description: "Verify nanoda detects the package module from current lakefile.toml syntax" +description: "Verify nanoda detects the lean_lib module from current lakefile.toml syntax" inputs: toolchain: description: "Lean toolchain used by the generated test package" @@ -17,21 +17,34 @@ runs: - name: create a TOML Lake package run: | lake init nanodatoml .toml - lake update + echo "lakefile.toml:" + cat lakefile.toml 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 + # 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: - 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 + 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 diff --git a/scripts/run_nanoda.sh b/scripts/run_nanoda.sh index 5cc56b0..9fd1689 100755 --- a/scripts/run_nanoda.sh +++ b/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,7 @@ 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 - # 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" - -# 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" @@ -104,7 +122,7 @@ 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"