`--serial` mode crashes before prover phase: `local: can only be used in a function`

[TengshunYang]

Summary

Running archon-loop.sh with --serial crashes at the start of Phase 2 (Prover) with a bash error. The plan phase completes normally, but the prover never runs.

Introduced in PR #8 (be26bca). The snapshot baseline code added to the serial branch uses local at top-level scope.

Version

Commit: be26bca24d00ddf96b65a573aea6e0a596d40700 (latest main)

Environment

• OS: Linux 6.6.87.2-microsoft-standard-WSL2
• Bash: GNU bash 5.2.21(1)-release
• Lean: 4.29.0
• Lake: 5.0.0-src+98dc76e

Reproduction

Project 1: single trivial theorem

A minimal Lean project with one sorry:

```lean
namespace MinimalArchonExample

theorem addZeroRight (n : Nat) : n + 0 = n := by
sorry

theorem zeroAddLeft (n : Nat) : 0 + n = n := by
simp

end MinimalArchonExample
```

After init.sh and running with --serial:

```bash
./archon-loop.sh {project_path} --max-iterations 1 --serial
```

Project 2: multi-line induction proofs

A Lean project with two theorems requiring induction:

```lean
namespace ArchonTest2

def rev : List α → List α
| [] => []
| x :: xs => rev xs ++ [x]

theorem rev_append (xs ys : List α) :
rev (xs ++ ys) = rev ys ++ rev xs := by
sorry

theorem rev_rev (xs : List α) :
rev (rev xs) = xs := by
sorry

end ArchonTest2
```

After init.sh, ensure .archon/PROGRESS.md has stage prover and Current Objectives references ArchonTest2/Basic.lean.

```bash
./archon-loop.sh {project_path} --max-iterations 1 --serial --no-review
```

Output:

```
[ARCHON] Phase 1: Plan agent
[ARCHON] ────────────────────────────────────────
...
[ARCHON] Plan phase finished. (125s)

[ARCHON] Phase 2: Prover agent(s)
[ARCHON] ────────────────────────────────────────
./archon-loop.sh: line 810: local: can only be used in a function
```

Script exits with code 1. The prover never starts.

This was reproduced 3 times on this project. The bug triggers every time.

Note: without --serial, the same project runs the prover phase normally and successfully proves both theorems.

Trigger conditions

The bug triggers when both conditions are met:

1. There are actual sorry targets for the prover to work on (if the project is COMPLETE, the loop exits before reaching the serial branch)
2. --serial flag is used

Root cause

In archon-loop.sh, the serial prover code path (lines 810–821) uses local in the top-level for loop body, outside any function. Bash only allows local inside functions.

This code was added in PR #8 (be26bca) as part of the snapshot baseline feature. The parallel branch (run_parallel_provers function) uses local correctly because it is inside a function.

```bash

archon-loop.sh, lines 809-821 (inside top-level for loop, NOT inside a function)

    else
        # -- Snapshot: baseline for all target files in serial mode --
        local sorry_files_serial                          # <-- line 810
        sorry_files_serial=$(parse_objective_files)
        if [[ -n "$sorry_files_serial" ]]; then
            while IFS= read -r sf; do
                local srel                                # <-- line 814
                srel=$(relpath "$sf" "$PROJECT_PATH")
                local sslug                               # <-- line 816
                sslug=$(echo "$srel" | sed 's|/|_|g; s|\.lean$||')
                local ssnap="${ITER_DIR}/snapshots/${sslug}"  # <-- line 818
                mkdir -p "$ssnap"
                cp "$sf" "${ssnap}/baseline.lean" 2>/dev/null || true
            done <<< "$sorry_files_serial"
        fi

```

With set -euo pipefail (line 2), the local error is fatal and terminates the script.

Note: bash -n archon-loop.sh passes because local outside a function is a runtime error, not a syntax error.

Workaround

Omit --serial. For single-file projects, the default parallel mode effectively runs one prover and produces the same result.