fix: remove stale nanoda-on-main-only docs, improve module detection

- Remove references to nanoda-on-main-only input from README (was
  removed in 8865ac2)
- Allow leading whitespace when detecting package name in lakefile.lean

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: kim-em

README.md

@@ -216,12 +216,6 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Default: "true"
     nanoda-allow-sorry: ""
 
-    # Only run nanoda on push events to the default branch, not on pull requests.
-    # Useful for reducing CI time on PRs since nanoda verification is slow.
-    # Allowed values: "true" | "false".
-    # Default: "true"
-    nanoda-on-main-only: ""
-
     # Enable GitHub caching.
     # Allowed values: "true" or "false".
     # If use-github-cache input is not provided, the action will use GitHub caching by default.
@@ -333,15 +327,6 @@ steps:
     nanoda: true
 ```
 
-By default, nanoda only runs on push events to the main branch (not on PRs) because verification adds significant CI time. To run on all events:
-
-```yaml
-- uses: leanprover/lean-action@v1
-  with:
-    nanoda: true
-    nanoda-on-main-only: false
-```
-
 ### Require no sorry placeholders
 
 By default, nanoda permits the `sorryAx` axiom for projects with incomplete proofs. To require all proofs be complete:

scripts/run_nanoda.sh

@@ -69,8 +69,8 @@ fi
 
 # Fallback to lakefile.lean
 if [ -z "$MODULE_NAME" ] && [ -f "lakefile.lean" ]; then
-    # Try to extract from 'package' declaration
-    MODULE_NAME=$(grep -E "^package\s+" lakefile.lean | head -1 | awk '{print $2}' || true)
+    # 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