[SMC17]

This PR fixes nanoda module discovery for current Lake TOML projects.

lake init name .toml emits a top-level package name and a distinct [[lean_lib]] module name. The nanoda runner previously searched only for a legacy [package] section and failed before independent checking. Reading the package name alone would also be incorrect when its spelling differs from the Lean module root.

The detector now prefers the first lean_lib name and retains the old first-name fallback for compatibility. A functional test generates a standard TOML package and requires the nanoda status to be SUCCESS with sorryAx disabled.

Supersedes #168: that branch had diverged from main and GitHub marked it CONFLICTING even though the intended file-level change is these four paths. This branch is current leanprover/main plus:

• scripts/run_nanoda.sh — prefer [[lean_lib]] name
• CHANGELOG.md — Unreleased note
• .github/workflows/functional_tests.yml — nanoda-toml-package job
• .github/functional_tests/nanoda_toml/action.yml — fixture

Configurable nanoda module selection remains out of scope here and is tracked in #179 / #180.

[SMC17]

Ready for review. GitHub has not started Actionlint / Functional Tests / ShellCheck on this fork PR (action_required — first-time contributor). A maintainer Approve and run workflows is the next click.

What this PR does: lake init foo .toml currently has package name foo and lean_lib name Foo. nanoda has to export the module, not the package. scripts/run_nanoda.sh now prefers the first [[lean_lib]] name.

What this PR does not do: it does not fix nanoda Error: invalid digit found in string on current Lean 4.28 export (that is #169 / #177, debug-branch NDJSON). The new nanoda-toml-package job asserts detection (Nanodatoml vs nanodatoml) only.

Preview on the fork (including nanoda-toml-package green in 24s): https://github.com/SMC17/lean-action/actions/runs/32407274723

[Unjuno]

Adding an end-to-end downstream reproduction for the TOML module-discovery gap addressed here.

The pinned OpenAI NavierStokesAndEuler lakefile (f9e8bc5b38b6e212696e8a30e3e91517af887bbd) has a top-level package name and three [[lean_lib]] declarations (NavierStokes, Euler, ComparatorChallenges). Our audit used lean-action at f061402b660e0c34644504b324e830f2991d4865; the hosted run failed with the annotation Could not detect module name from lakefile.toml or lakefile.lean (run 37240186684).

I fetched both immutable source files and replayed the detector extraction from that action revision: it returns an empty module name for the OpenAI lakefile, while the three lean_lib names are present. The hash-verified reproduction and scope limits are recorded in the benchmark repository.

This looks like a useful real-project case for the [[lean_lib]] detector change in #187. The failed run does not diagnose the separate export-format issue or provide evidence about the Lean theorem itself; its public page exposes the module-detection annotation, but not detailed step logs.