backend: CoqInterface always proves on a copy

Proving on a scratch copy was arranged by each entry point: main.py and
test_folder_batch each built a ScratchProof, swapped the path, and passed
source_path so records would still name the original. Every other caller
-- 17 of the 19 construction sites -- got no copy at all, and the default
was the destructive one.

There is no read-only mode to justify that. load() alone pops the trailing
"Admitted.", clear_all_proof_scripts() rewrites the file, and coqpyt
writes every accepted tactic straight to disk. Any CoqInterface built on a
file the caller cares about will damage it.

So the copy moves into the constructor, and both knobs disappear with it:

  - work_on_copy is gone: there is nothing to opt out of.
  - source_path is gone: the file you pass IS the source, so the interface
    derives it. The question "when is source_path None?" no longer exists.

ScratchProof now has exactly one caller. Nothing else in the tree
references it.

Two things had to move, because they edited the file before a copy
existed and would otherwise have hit the user's own file: the Hammer
import injection, and proof cleaning. Both now run between construction
and load(), on coq_interface.file_path, with clean_success threaded back
through the components dict. Saving became coq_interface.save_result(),
behind a _harvest_proof() helper the signal handler and the normal exit
both use.

Scratch cleanup is registered with atexit rather than done in close(),
because load() calls close() to tear down the previous coq-lsp session
and would otherwise delete the file out from under itself.
ScratchProof.close() only unlinks files, so it is safe at interpreter
exit.

Also drops getattr(self.coq, 'source_path', None) in ProofController. The
attribute is always set, and the None fallback resolved to
proof_file.path -- the scratch name, the exact value the feature exists to
keep out of records.

Verified end to end against a real run (gpt-4.1):

    🎉 Proof completed successfully!
    examples/example.v                      a380c035 -> a380c035  (untouched)
    examples/autorocq-20260901-153147/example.v   holds the found proof
    stray *_autorocq_*.v                    none

Full suite: 34 passed, 1 skipped, 3 errors -- the errors pre-existing and
fixed separately.

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

Author: dingf3ng

proof-search/agent/proof_controller.py

@@ -228,7 +228,7 @@ def _init_proof_session(self, theorem_name: str = None) -> bool:
                     proof_file=proof_file,
                     theorem_name=self.current_theorem_name,
                     metadata={'max_steps': self.max_steps, 'controller_version': '1.0'},
-                    proof_file_path=getattr(self.coq, 'source_path', None)
+                    proof_file_path=self.coq.source_path
                 )
             except Exception as e:
                 self.logger.error(f"❌ Failed to start proof recording: {e}")

proof-search/backend/coq_interface.py

@@ -1,5 +1,6 @@
 # backend/coq_interface.py
 
+import atexit
 import os
 import re
 import signal
@@ -10,6 +11,7 @@
 from pathlib import Path
 from contextlib import contextmanager
 from utils.logger import setup_logger, clean_ansi_codes
+from utils.scratch import ScratchProof
 
 
 class CoqSessionDesync(RuntimeError):
@@ -24,21 +26,31 @@ def __init__(self, file_path: str, workspace: Optional[str] = None,
                  library_paths: Optional[List[Dict[str, str]]] = None,
                  auto_setup_coqproject: bool = False,
                  coqproject_extra_options: Optional[List[str]] = None,
-                 timeout: int = 10,
-                 source_path: Optional[str] = None):
+                 timeout: int = 10):
         """
         Initialize Coq interface.
         
         NEW PARAMETERS:
         - library_paths: List of library mappings [{"path": "/path", "name": "libname"}, ...]
         - auto_setup_coqproject: Whether to automatically create/update _CoqProject
         - coqproject_extra_options: Additional options for _CoqProject
-        - source_path: The file this one is a scratch copy of, when it is one.
-          Proofs are run on a throwaway copy (see utils/scratch.py), so records
-          and reports must name the original rather than the copy.
+
+        There is no read-only mode: load() alone pops the trailing "Admitted.",
+        clear_all_proof_scripts() rewrites the file, and coqpyt writes every
+        accepted tactic straight to disk. So file_path is never touched -- it is
+        the source, and all work happens on a copy beside it. source_path names
+        the original for anything that reports or records a proof; file_path is
+        the copy the agent actually edits. Call save_result() for the outcome.
         """
-        self.file_path = os.path.abspath(file_path)
-        self.source_path = os.path.abspath(source_path) if source_path else self.file_path
+        self.source_path = os.path.abspath(file_path)
+        self.logger = setup_logger("CoqInterface")
+
+        self._scratch = ScratchProof(file_path, self.logger)
+        self.file_path = str(self._scratch.open())
+        # Not in close(): load() calls close() to tear down the previous coq-lsp
+        # session and would delete the file out from under itself.
+        # ScratchProof.close() only unlinks files, so it is safe at exit.
+        atexit.register(self._scratch.close)
         if workspace is not None and not os.path.isabs(workspace):
             workspace = os.path.abspath(workspace)
         self.workspace = workspace
@@ -52,7 +64,6 @@ def __init__(self, file_path: str, workspace: Optional[str] = None,
         self.proof_file = None
         self.proof = None
         self.last_error = None
-        self.logger = setup_logger("CoqInterface")
 
         # Cache for recent goal queries so we avoid back-to-back LSP `proof_goals` calls
         # when the proof state hasn't changed.
@@ -992,6 +1003,10 @@ def close(self):
             self.logger.warning(f"Error during CoqInterface close: {e}")
             # Don't raise - just log and continue
 
+    def save_result(self, dest_dir, name: Optional[str] = None):
+        """Copy the proof the agent produced into dest_dir. Returns the path."""
+        return self._scratch.save(dest_dir, name)
+
     def force_close(self):
         try:
             self.logger.info("Forcing coq-lsp shutdown...")

proof-search/main.py

@@ -23,7 +23,6 @@
 
 from utils.config import load_config, ProofAgentConfig
 from utils.logger import setup_logger, global_logger
-from utils.scratch import ScratchProof
 
 
 def parse_arguments():
@@ -202,27 +201,39 @@ def initialize_components(args, config: ProofAgentConfig, logger) -> Dict[str, A
                 logger.info(f"   - {lib['name']}: {lib['path']}")
             logger.info(f"🔧 Auto setup CoqProject: {getattr(config.coq, 'auto_setup_coqproject', True)}")
 
-        # If hammer is enabled, add hammer library import to proof file
-        if config.enable_hammer:
-            logger.info("🔧 Hammer enabled. Importing hammer library...")
-            with open(args.proof_file, 'r', encoding='utf-8') as f:
-                content = f.read()
-            if "From Hammer Require Import Hammer." not in content:
-                with open(args.proof_file, 'w', encoding='utf-8') as f:
-                    f.write("From Hammer Require Import Hammer.\nFrom Hammer Require Import Tactics.\n\n" + content)
-            else:
-                logger.debug("🔧 Hammer already imported - skipping")
-        
         coq_interface = CoqInterface(
             file_path=args.proof_file,
-            source_path=config.coq.proof_file_path,
             workspace=workspace,
             library_paths=library_paths,
             auto_setup_coqproject=getattr(config.coq, 'auto_setup_coqproject', True),
             coqproject_extra_options=coqproject_extra_options,
             timeout=getattr(config.coq, 'timeout', 60)
         )
 
+        # Everything below edits the file, so it has to come after the
+        # constructor -- that is what puts the scratch copy in place.
+        scratch_file = coq_interface.file_path
+
+        if config.enable_hammer:
+            logger.info("🔧 Hammer enabled. Importing hammer library...")
+            with open(scratch_file, 'r', encoding='utf-8') as f:
+                content = f.read()
+            if "From Hammer Require Import Hammer." not in content:
+                with open(scratch_file, 'w', encoding='utf-8') as f:
+                    f.write("From Hammer Require Import Hammer.\nFrom Hammer Require Import Tactics.\n\n" + content)
+            else:
+                logger.debug("🔧 Hammer already imported - skipping")
+
+        # Clean proof by removing existing tactics. Skip in interactive mode
+        if config.interactive.enabled:
+            logger.debug("🤝 Interactive mode enabled - preserving existing proof tactics")
+            clean_success = ensure_proof_admitted(scratch_file, logger)
+        else:
+            logger.debug("🧹 Pre-cleaning proof file to ensure unproven state...")
+            clean_success = clean_proof_file(scratch_file, logger)
+            if not clean_success:
+                logger.warning("⚠️ Could not clean proof file - will try CoqInterface methods later")
+
         # Load the file using proper method
         success = coq_interface.load()
         if not success:
@@ -291,7 +302,8 @@ def initialize_components(args, config: ProofAgentConfig, logger) -> Dict[str, A
             "coq_interface": coq_interface,
             "context_manager": context_manager,
             "coq_chat_session": context_manager.chat_session,
-            "controller": controller
+            "controller": controller,
+            "clean_success": clean_success
         }
 
     except Exception as e:
@@ -553,14 +565,24 @@ def clean_proof_file(file_path: str, logger) -> bool:
         return False
 
 
+def _harvest_proof(components, output_dir, logger):
+    """Save whatever the agent proved into the run's output directory."""
+    coq_interface = (components or {}).get("coq_interface")
+    if coq_interface is None:
+        return
+    try:
+        coq_interface.save_result(output_dir)
+    except Exception as e:
+        logger.warning(f"Could not save the resulting proof: {e}")
+
+
 def main():
     """Main entry point with history management."""
 
-    global components, logger, exit_code, scratch
+    global components, logger, exit_code
     components = {}
     logger = None
     exit_code = 1
-    scratch = None
 
     def signal_handler(signum, frame):
         sig_name = signal.Signals(signum).name
@@ -569,10 +591,8 @@ def signal_handler(signum, frame):
         if components and logger:
             cleanup_components(components, logger)
 
-        if scratch:
-            scratch.save(output_dir)
-            scratch.close()
-        
+        _harvest_proof(components, output_dir, logger)
+
         sys.exit(128 + signum)
 
     # Register signal handlers
@@ -661,24 +681,6 @@ def signal_handler(signum, frame):
     if args.interactive:
         config.interactive.enabled = True
 
-    # Prove on a throwaway copy. Cleaning below strips the existing tactics and
-    # coqpyt writes every accepted tactic back to disk, so the file being proved
-    # must never be the user's own. config.coq.proof_file_path keeps pointing at
-    # the original, which is what reporting and recording should name.
-    scratch = ScratchProof(args.proof_file, logger)
-    scratch.open()
-    args.proof_file = str(scratch.path)
-
-    # Clean proof by removing existing tactics. Skip in interactive mode
-    if config.interactive.enabled:
-        logger.debug("🤝 Interactive mode enabled - preserving existing proof tactics")
-        clean_success = ensure_proof_admitted(args.proof_file, logger)
-    else:
-        logger.debug("🧹 Pre-cleaning proof file to ensure unproven state...")
-        clean_success = clean_proof_file(args.proof_file, logger)
-        if not clean_success:
-            logger.warning("⚠️ Could not clean proof file - will try CoqInterface methods later")
-
     # Initialize components
     try:
         components = initialize_components(args, config, logger)  # Pass both args and config
@@ -689,6 +691,7 @@ def signal_handler(signum, frame):
 
         # Log final proof file verification
         coq_interface = components["coq_interface"]
+        clean_success = components["clean_success"]
         logger.info(f"✅ Coq interface loaded: {coq_interface.file_path}")
 
         if not clean_success and not config.interactive.enabled:
@@ -798,10 +801,8 @@ def signal_handler(signum, frame):
 
         cleanup_components(components, logger)
 
-        # Coq session is closed, so the scratch file is safe to harvest and remove.
-        if scratch:
-            scratch.save(output_dir)
-            scratch.close()
+        # Coq session is closed, so the scratch copy is safe to harvest.
+        _harvest_proof(components, output_dir, logger)
 
     sys.exit(exit_code)
 

proof-search/tests/test_folder_batch.py

@@ -16,7 +16,6 @@
 from agent.context_manager import ContextManager
 from agent.proof_controller import ProofController
 from utils.config import ProofAgentConfig
-from utils.scratch import ScratchProof
 
 # --- CONFIGURATION ---
 # Folder containing .v files to prove
@@ -87,18 +86,11 @@ def prove_single_file(
     crash_count = 0
 
     while crash_count < max_crash_retries:
-        scratch = ScratchProof(coq_file)
+        coq_interface = None
         try:
-            scratch.open()
-            
-            # Clean the scratch copy, never the benchmark file itself
-            if not clean_proof_file(scratch.path):
-                return False
-            
-            # Initialize CoqInterface
+            # CoqInterface proves on a copy, so the benchmark file is never touched.
             coq_interface = CoqInterface(
-                file_path=str(scratch.path),
-                source_path=str(coq_file),
+                file_path=str(coq_file),
                 workspace=config.coq.workspace or str(Path(coq_file).parent),
                 library_paths=config.coq.library_paths,
                 auto_setup_coqproject=config.coq.auto_setup_coqproject,
@@ -107,6 +99,9 @@ def prove_single_file(
             )
 
             try:
+                if not clean_proof_file(coq_interface.file_path):
+                    return False
+
                 # Load the cleaned file
                 if not coq_interface.load():
                     return False
@@ -161,9 +156,8 @@ def prove_single_file(
                 raise e
 
         finally:
-            if results_dir is not None:
-                scratch.save(results_dir, result_name)
-            scratch.close()
+            if coq_interface is not None and results_dir is not None:
+                coq_interface.save_result(results_dir, result_name)
 
     return False