fix: serialize Lean REPL access and pinpoint search-tactic feedback

[KrystianNowakowski]

Summary

Two experiment-robustness fixes split out of #35 so they can be reviewed and merged
independently. Both surfaced during larger-scale experiment runs and are model-agnostic
(nothing DeepSeek-specific).

Serialize LeanInteract REPL access with a per-command lock

The single AutoLeanServer subprocess is shared by all concurrent experiment samples, but
run() only locked server creation, not command execution. Firing many full-Mathlib
FileCommands at one REPL at once races the subprocess and trips its memory backstop,
surfacing as spurious LeanErrors (the 0-iteration startup crashes). A per-command run
lock serializes execution; lake builds are unaffected (separate subprocesses).

Pinpoint search-tactic feedback and surface fatal Lean errors

• SearchTacticsDetectedFeedback dumped the entire declaration as its "Locations", so the
  prover could not tell which tactic was flagged and stripped innocent tactics
  (field_simp, apply) out of a compiling proof. Each offending tactic is now reported
  with its line number. The detection regex itself is unchanged.
• A file that fails to compile comes back from lean_interact as a LeanError (message
  only, no declarations), so list_declarations_from_* blew up with an opaque
  AttributeError on .declarations. It now detects LeanError and raises the actual
  Lean compile message.

Tests

Adds/keeps coverage: test_lean_interact.py (lock serializes concurrent commands),
test_cheat_detection.py (per-line tactic reporting, innocent tactics not flagged),
test_lean_parsing.py (fatal LeanError → clear RuntimeError). Full unit suite green.

---

Note

Medium Risk
Serializing all LeanInteract commands can increase latency under heavy parallelism, but it fixes correctness of shared REPL use; parsing and feedback changes are localized with new unit tests.

Overview
Hardens concurrent experiment runs and prover feedback when Lean parsing or cheat detection fails.

LeanInteract now holds a per-command asyncio lock so only one REPL command runs at a time on the shared subprocess, avoiding races and spurious LeanErrors when many samples hit the same server.

Search-tactic rejection no longer puts the full declaration in SearchTacticsDetectedFeedback.locations; it lists each flagged tactic as line N: <tactic> so the prover can fix only simp? / exact?-style lines instead of rewriting the whole proof.

Declaration listing routes REPL results through _bundle_response, which raises RuntimeError with Lean’s message when the response is a fatal LeanError (e.g. bad import) instead of failing on missing .declarations.

^{Reviewed by Cursor Bugbot for commit 22fa709. Bugbot is set up for automated code reviews on this repo. Configure here.}