No automatic re-scan when sorries are added back after project is marked COMPLETE

[TengshunYang]

Summary

When a project reaches COMPLETE status, archon-loop.sh exits immediately without checking actual code state. If a user later modifies .lean files — changing a proof back to sorry, editing a theorem statement, or adding new theorems — Archon has no way to detect the mismatch and will refuse to run.

This is a design gap: there is no watchdog, hook, or pre-flight check that compares live sorry count against the recorded stage in PROGRESS.md.

Reproduction

1. Initialize a minimal Lean project and run Archon to completion:

namespace MinimalArchonExample

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

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

end MinimalArchonExample

cd /path/to/Archon
./init.sh /path/to/project
./archon-loop.sh /path/to/project --max-iterations 3

Archon proves addZeroRight, marks project COMPLETE. .archon/PROGRESS.md now reads:

## Current Stage
COMPLETE

2. Manually revert the proof back to sorry:

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

3. Re-run Archon:

./archon-loop.sh /path/to/project --max-iterations 1

4. Observed behavior:

[ARCHON]  Project 'project' is COMPLETE. Nothing to do.

Archon exits immediately. The plan agent never runs, so the new sorry is never detected.

Expected behavior

Archon should detect that .lean files contain sorries despite the project being marked COMPLETE, and either:

• Automatically revert the stage and re-enter the proving loop, or
• Warn the user about the mismatch and suggest how to proceed

Suggestion

A lightweight pre-flight sorry check before the COMPLETE early-exit in archon-loop.sh could address this. For example, running sorry_analyzer.py and comparing the result against the recorded stage — if sorries exist but the stage is COMPLETE, either auto-revert or warn.

[surenny]

I've hit this as well. While there's no native fix yet, here's a workaround that avoids modifying Archon's code:

1. Edit USER_HINTS.md in .archon/ to inform the system that new sorries have been introduced (e.g., "I have added a new sorry in Foo.lean, please prove it").

2. Launch the loop with --stage prover:

   ./archon-loop.sh /path/to/project --stage prover

   This overrides the COMPLETE status that the script reads from PROGRESS.md and forces it to spawn the Plan agent.

3. The Plan agent will see that PROGRESS.md says COMPLETE, but it also reads USER_HINTS.md. In most cases, it recognizes the mismatch and reverts the stage back to prover, then proceeds to fill in the sorry through the normal loop.

Not a proper fix, but it gets the job done without rewriting the shell script.