agent: add --output-dir, and say where the proof actually lands

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>

Author: 2 people

README.md

@@ -107,7 +107,7 @@ If AutoRocq runs successfully, you will be able to see in the terminal
 ```
 [INFO] [Main]: 🎉 Proof completed successfully!
 ```
-and the proof script is saved in the same [`example.v`](proof-search/examples/example.v) file. You will also be able to find saved proof states and aggregated results at `data/`, which can be reused to prove other goals in the future.
+The proof runs on a throwaway copy, so [`example.v`](proof-search/examples/example.v) itself is left untouched; the resulting proof script is written to the run's output directory, `examples/autorocq-<timestamp>/example.v` by default (use `--output-dir` to choose your own). You will also be able to find saved proof states and aggregated results at `data/`, which can be reused to prove other goals in the future.
 
 For more configurations of the tool, check out the [readme](proof-search/configs/readme.md) or run with `--help` for more options.
 

proof-search/main.py

@@ -93,6 +93,12 @@ def parse_arguments():
         help="Set workspace directory"
     )
 
+    parser.add_argument(
+        "--output-dir",
+        help="Directory for this run's artifacts: the log, the resulting proof, "
+             "and the proof tree (default: autorocq-<timestamp> beside the proof file)"
+    )
+
     parser.add_argument(
         "--local-session-caching",
         action="store_true",
@@ -160,7 +166,7 @@ def setup_output_directory(output_dir: Optional[str]) -> Path:
         proof_file_path = Path(sys.argv[1]) if len(sys.argv) > 1 else Path(".")
         output_path = proof_file_path.parent / f"autorocq-{datetime.now().strftime('%Y%m%d-%H%M%S')}"
 
-    output_path.mkdir(exist_ok=True)
+    output_path.mkdir(parents=True, exist_ok=True)
     return output_path
 
 
@@ -610,7 +616,7 @@ def signal_handler(signum, frame):
         sys.exit(1)
 
     # Setup output directory
-    output_dir = setup_output_directory(config.output_dir)
+    output_dir = setup_output_directory(args.output_dir or config.output_dir)
 
     # Use absolute path
     args.proof_file = str(Path(args.proof_file).resolve())