agent: prove on a scratch copy, not the user's file - #9
Open
dingf3ng wants to merge 2 commits into
Open
Conversation
dingf3ng
force-pushed
the
agent-scratch-proof
branch
2 times, most recently
from
September 2, 2026 07:36
695ee6c to
60095ea
Compare
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>
dingf3ng
force-pushed
the
agent-scratch-proof
branch
from
September 2, 2026 07:57
60095ea to
f1cae66
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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
.vin AutoRocq-bench — which is why the standing advice aftertest_folder_batchhas beengit -C AutoRocq-bench checkout -- benchmarks.What changed
utils/scratch.py—ScratchProofhands the agent a throwaway copy:_CoqProject, same sibling modules, same library pathsThe knock-on
The file being proved now has a generated name, so anything that reports a proof has to be told the original:
CoqInterfacesource_path, defaults tofile_path— non-scratch callers unaffectedProofRecorder.start_proof_recordingproof_file_path; records are grouped by file, so a scratch name would scatter themProofControllercoq.source_paththroughmain.pyharvests 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_batchdoes the same per file..gitignorecovers*_autorocq_*.v, so a scratch file left by a hard kill can't be mistaken for a source file.