fix: detect TOML lean_lib modules for nanoda

[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.

[petr-kratochvil]

I just came across this PR and I was thinking, what about having the module name configurable?

The use case: a project where only part of it should be checked by nanoda. For example, a "clean" mathematical part (should be checked) and an algorithmic/monadic/native_decide-heavy part.

[petr-kratochvil]

I think that the # Fallback to lakefile.lean section at run_nanoda.sh should be also updated to prioritize lean_lib before package (for consistency)...

[petr-kratochvil]

I just came across this PR and I was thinking, what about having the module name configurable?

Created a separate issue for it: #179

[SMC17]

Rebased onto current main (resolved CHANGELOG conflict with the portable-shebang fix). Still draft until functional tests go green.

[SMC17]

Updated this branch so the four changed files are current-main plus the nanoda TOML fix:

• scripts/run_nanoda.sh — prefer [[lean_lib]] name
• CHANGELOG.md — Unreleased note next to the portable-shebang fix
• .github/workflows/functional_tests.yml — nanoda-toml-package job on the current workflow
• .github/functional_tests/nanoda_toml/action.yml — fixture

GitHub still marks the PR CONFLICTING because the branch is 7 commits behind main (fork main could not be fast-forwarded from this token). A maintainer Update branch / merge from the UI should apply cleanly; the file-level diffs vs main are only those four paths.

[SMC17]

Superseded by #187.

This branch had diverged from main and GitHub kept it CONFLICTING. #187 is current leanprover/main plus the same four-file nanoda TOML fix.

[SMC17]

Closing in favor of #187.