agent: prove on a scratch copy, not the user's file by dingf3ng · Pull Request #9 · NUS-Program-Verification/AutoRocq

dingf3ng · 2026-09-01T13:45:07Z

Why

The agent proves in place. clean_proof_file() strips the existing tactics from the target .v, then coqpyt writes every accepted tactic straight back to disk.

Pointed at a real file, a run destroys it: the original proof is gone and the working tree is dirty. A single benchmark run rewrites every .v in AutoRocq-bench — which is why the standing advice after test_folder_batch has been git -C AutoRocq-bench checkout -- benchmarks.

What changed

utils/scratch.py — ScratchProof hands the agent a throwaway copy:

created beside the original, so the workspace resolves exactly as before — same _CoqProject, same sibling modules, same library paths
given a module-safe generated name
on exit, the finished proof is saved into the run's output directory, where it stays available for independent re-checking instead of being clobbered by the next run
scratch file and its build artifacts removed

The knock-on

The file being proved now has a generated name, so anything that reports a proof has to be told the original:

call site	change
`CoqInterface`	takes `source_path`, defaults to `file_path` — non-scratch callers unaffected
`ProofRecorder.start_proof_recording`	takes `proof_file_path`; records are grouped by file, so a scratch name would scatter them
`ProofController`	passes `coq.source_path` through

main.py harvests the scratch copy on both exits — the normal one and the signal handler — so a Ctrl-C still keeps whatever the run had proved. test_folder_batch does the same per file.

.gitignore covers *_autorocq_*.v, so a scratch file left by a hard kill can't be mistaken for a source file.

zhaohuanqdcn · 2026-09-07T11:13:18Z

+        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.


This comment does not seem very useful

zhaohuanqdcn · 2026-09-07T11:20:50Z

        if components and logger:
            cleanup_components(components, logger)

+        _harvest_proof(components, output_dir, logger)


output_dir is not available here

zhaohuanqdcn · 2026-09-07T11:25:35Z

+        # 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)


I think atexit only fires when the Python process exits, not at the end of coq_interface objects

zhaohuanqdcn · 2026-09-07T11:26:46Z

+        while dest.exists():
+            dest = dest.with_name(f"{dest.stem}.{counter}{dest.suffix}")
+            counter += 1


This will save a.v -> a.1.v -> a.1.2.v as dest.stem is different each time

zhaohuanqdcn · 2026-09-07T11:29:58Z

+from typing import Optional, Union
+
+# Artifacts Coq leaves beside a .v file; they belong to the scratch copy.
+_BUILD_SUFFIXES = (".vo", ".vok", ".vos", ".glob", ".aux")


.aux is created as .name.aux, which cannot be matched.
Also double check that this does not include persistent coqpyt cache at the path.

zhaohuanqdcn · 2026-09-07T11:32:47Z

+        # Everything below edits the file, so it has to come after the
+        # constructor -- that is what puts the scratch copy in place.


Write: In-file edits should live in the scratch copy

zhaohuanqdcn · 2026-09-07T11:36:19Z

+        if config.interactive.enabled:
+            logger.debug("🤝 Interactive mode enabled - preserving existing proof tactics")
+            clean_success = ensure_proof_admitted(scratch_file, logger)


Interactive mode was designed to keep incremental progress, resuming half way without clean_proof_file. Now with scratch, the progress from each session is never flushed to the file. This is probably fine for this PR, but please open an issue to document it.

zhaohuanqdcn · 2026-09-07T11:39:30Z

Is this still needed? It seems like clean_proof_file is always called on a scratch copy?

zhaohuanqdcn · 2026-09-07T11:42:23Z

 proof-search/examples/coqpyt_aux_*
 proof-search/configs/local.json

+*_autorocq_*.v


This does not cover scratch files in the submodule

I will make a PR to benchmark repo later. :)

NUS-Program-Verification/AutoRocq-bench#2

zhaohuanqdcn · 2026-09-07T11:44:50Z

            else:
                failed_count += 1
                result_text = "No"



add assertion for scratch file invariants: original .v is intact, and temp objects are cleaned up

The agent proves in place. clean_proof_file() strips the existing tactics from the target .v, and coqpyt then writes every accepted tactic straight back to disk. Pointed at a real file, a run destroys it: the original proof is gone and the working tree is dirty. A single benchmark run rewrites every .v in AutoRocq-bench that way, which is why the standing advice after test_folder_batch has been `git -C AutoRocq-bench checkout -- benchmarks`. ScratchProof (utils/scratch.py) hands the agent a throwaway copy instead. The copy is created beside the original, so the workspace resolves exactly as before -- same _CoqProject, same sibling modules, same library paths -- and it is given a module-safe generated name. When the run ends the finished proof is saved into the run's output directory, where it stays available for independent re-checking rather than being clobbered by the next run, and the scratch file and its build artifacts are removed. The copy is made in CoqInterface's constructor, so every one of the 19 construction sites gets it and there is no knob to forget. No read-only mode would justify an opt-out: load() alone pops the trailing "Admitted.", clear_all_proof_scripts() rewrites the file, and coqpyt writes every accepted tactic straight to disk, so any CoqInterface built on a file the caller cares about would damage it. The file you pass IS the source, so the interface derives the source path rather than taking one -- the question "when is source_path None?" never arises. 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 that the signal handler and the normal exit both use, so a Ctrl-C still keeps whatever the run had proved. ProofRecorder.start_proof_recording takes proof_file_path: records are grouped by file, and a generated scratch name would scatter them. 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. .gitignore covers *_autorocq_*.v so a scratch file left behind by a hard kill cannot be mistaken for a source file. Verified end to end against a real run (gpt-4.1): 🎉 Proof completed successfully! examples/example.v a380c035 -> a380c035 (untouched) Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Proving on a scratch copy changes the behaviour the README documents. The quickstart still promised "the proof script is saved in the same example.v file" which was true, and was the reason example.v arrived in the tree already proven (a4c1e2f committed the output of running that very command). It is not true any more: the source file is left untouched and the result is written into the run's output directory. The rewritten paragraph names where the proof lands and offers --output-dir for choosing somewhere else. That flag did not exist: main.py read output_dir from the config file and nothing else, so the sentence documented something imaginary. Adding it is the smaller fix, and it is the flag a benchmark run wants -- without it every run drops its output directory next to the .v file, which for AutoRocq-bench means inside the submodule. It wins over the config the way every other command line option here already does, and the directory is created with parents so a path like /tmp/runs/today/first works. Checked: --help lists the flag, and setup_output_directory creates a nested path that does not exist yet. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

zhaohuanqdcn · 2026-09-07T13:45:55Z

+    """A disposable copy of a .v file, for one proof attempt."""
+
+    def __init__(self, source: Union[str, Path], logger=None):
+        self.source = Path(source).resolve()


This is different from the default os.path.abspath() resolution used in main, which does not follow symlinks. Make sure they are resolved in a consistent manner

LGTM now

dingf3ng force-pushed the agent-scratch-proof branch 3 times, most recently from 60095ea to f1cae66 Compare September 2, 2026 07:57

dingf3ng mentioned this pull request Sep 2, 2026

backend: CoqInterface always proves on a copy #14

Closed

zhaohuanqdcn mentioned this pull request Sep 7, 2026

tests: run every test against a temp copy #8

Merged

zhaohuanqdcn previously requested changes Sep 7, 2026

View reviewed changes

Base automatically changed from tests-temp-copies to main September 7, 2026 11:49

dingf3ng and others added 2 commits September 7, 2026 19:49

zhaohuanqdcn force-pushed the agent-scratch-proof branch from f1cae66 to 708b8c2 Compare September 7, 2026 11:49

zhaohuanqdcn reviewed Sep 7, 2026

View reviewed changes

zhaohuanqdcn added the enhancement New feature or request label Sep 7, 2026

dingf3ng added 3 commits September 7, 2026 16:40

agent: clean up scratch proofs when interfaces close

ee969e4

agent: handle signals before output setup

dd3a31d

agent: cover both aux artifact names

7ae4367

zhaohuanqdcn mentioned this pull request Sep 8, 2026

Interactive mode doesn't save the progress #20

Open

tests: remove invalid proof tree output reference

040eb60

zhaohuanqdcn merged commit db1f4bc into main Sep 8, 2026

zhaohuanqdcn deleted the agent-scratch-proof branch September 8, 2026 04:08

		# Everything below edits the file, so it has to come after the
		# constructor -- that is what puts the scratch copy in place.

Uh oh!

Conversation

dingf3ng commented Sep 1, 2026

Why

What changed

The knock-on

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants