backend: CoqInterface always proves on a copy

[dingf3ng]

Why

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 still named the original.

Every other caller — 17 of the 19 construction sites — got no copy at all. The destructive behaviour was the default.

There's 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 you care about will damage it.

What changed

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

• work_on_copy is gone — there's nothing to opt out of
• source_path is gone — the file you pass is the source, so the interface derives it

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

What had to move

Two things edited the file before a copy existed, and would otherwise have hit the user's own file:

	now runs
Hammer import injection	after construction, on coq_interface.file_path
proof cleaning	between construction and load(), clean_success threaded back through the components dict

Saving became coq_interface.save_result(), behind a _harvest_proof() helper shared by the signal handler and the normal exit.

Scratch cleanup is on atexit, not in close() — 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's 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

Real run against 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: 36 passed, 2 skipped, 0 errors.

[dingf3ng]

Folded into #9.

Splitting this from #9 meant introducing work_on_copy and source_path in #9 and deleting them here, four PRs later, and rewriting ~40 lines of main.py that #9 had just written. Nobody had reviewed either PR, so there was no reason to make a reviewer read that twice.

#9 now makes the copy in CoqInterface.__init__ directly — no intermediate opt-in API, and main.py is one coherent change instead of two overlapping ones. The end state is byte-identical: git diff between the old and new stack tips is empty.

#15's base has been repointed to #13 (tests-config-fixture), so the chain is unbroken.

🤖 Generated with Claude Code