Reopen reads after rejected range repair
Jaime Fournier <jaimef@linbsd.org>
b5708c7a3f39c0032c66c06f3dbc8ac31f0333af
diff --git a/src/jcode/core/verified-run.ss b/src/jcode/core/verified-run.ss
index 8a8c6cb..048d99f 100644
--- a/src/jcode/core/verified-run.ss
+++ b/src/jcode/core/verified-run.ss
@@ -5423,6 +5423,13 @@
msg
"\nThe replacement was not written; the on-disk file is unchanged. "
"Do not switch to a full-file edit/write. Retry the same local repair with syntax-correct replacement content:\n"
+ " read(path=\""
+ path
+ "\", start="
+ (number->string start-line)
+ ", end="
+ (number->string end-line)
+ ")\n"
" replace_range(path=\""
path
"\", start="
@@ -5436,6 +5443,10 @@
(let ((repair (current-required-range-repair))
(msg (jerboa-syntax-guard-message path full-content)))
(when msg
+ ;; A rejected bounded repair is a fresh local diagnostic, not another
+ ;; stale verifier observation. Give the model a narrow read window to
+ ;; inspect the implicated span before retrying the repair.
+ (current-inspections-after-failed-verify 0)
(if (and (not (current-verified-local-model?))
repair
(repair-path-matches? cwd repair path)
diff --git a/test/run.ss b/test/run.ss
index 70c0c12..047ee2d 100644
--- a/test/run.ss
+++ b/test/run.ss
@@ -10785,6 +10785,89 @@
(safe-delete-test-file! target-path))
(let* ([vr-dir "/tmp"]
+ [target "jcode-verified-replace-range-read-after-reject.ss"]
+ [target-path (string-append vr-dir "/" target)]
+ [initial "(import (jerboa prelude))\n(define (main)\n (let ((row (make-vector 1)))\n (vector-set! row 0 #t)\n (displayln \"ok\")))\n(main)\n"]
+ [bad-line " (vector-set!row 0 #f)"]
+ [good-line " (vector-set! row 0 #f)"]
+ [tool-results '()]
+ [slurp (lambda (p) (call-with-input-file p (lambda (i) (get-string-all i))))])
+ (safe-delete-test-file! target-path)
+ (write-test-output-file target-path
+ (lambda (o) (display initial o)) 'replace)
+ (let* ([scope (parse-write-scope target)]
+ [wf (coding-workflow (string-append "grep -q '#f' " target) vr-dir
+ (list (cons 'write-scope scope)))]
+ [read-call
+ (lambda ()
+ (list
+ (make-wtool-call
+ "read"
+ (list (cons "path" target)
+ (cons "start" 3)
+ (cons "end" 5))
+ #f)))]
+ [resp (scripted-responder
+ (list
+ (list (make-wtool-call "verify" '() #f))
+ (read-call)
+ (read-call)
+ (list
+ (make-wtool-call
+ "replace_range"
+ (list (cons "path" target)
+ (cons "start" 4)
+ (cons "end" 4)
+ (cons "content" bad-line))
+ #f))
+ (read-call)
+ (list
+ (make-wtool-call
+ "replace_range"
+ (list (cons "path" target)
+ (cons "start" 4)
+ (cons "end" 4)
+ (cons "content" good-line))
+ #f))
+ (list (make-wtool-call "verify" '() #f))
+ (list (make-wtool-call "done" '(("summary" . "replace-range-read-after-reject")) #f))))]
+ [result (parameterize ((current-write-scope scope))
+ (run-workflow wf "read after rejected replace_range syntax"
+ resp
+ (list (cons 'local-model? #t)
+ (cons 'max-iterations 10)
+ (cons 'max-tool-errors 3)
+ (cons 'on-message
+ (lambda (m)
+ (when (equal? (message-role m) "tool")
+ (set! tool-results
+ (cons (message-content m) tool-results))))))))])
+ (check! "verified-run: replace_range rejected syntax read recovers"
+ result "replace-range-read-after-reject")
+ (check-pred! "verified-run: replace_range rejection reopens target read"
+ (reverse tool-results)
+ (lambda (xs)
+ (let loop ([ys xs] [saw-reject #f])
+ (cond
+ [(null? ys) #f]
+ [(and saw-reject
+ (str-contains? (car ys) "(vector-set! row 0 #t)")
+ (not (str-contains? (car ys)
+ "inspection limit reached after failed verify")))
+ #t]
+ [else
+ (loop (cdr ys)
+ (or saw-reject
+ (and (str-contains? (car ys) "The replacement was not written")
+ (str-contains? (car ys) "read(path=\""))))]))))
+ (check-pred! "verified-run: replace_range read-after-reject writes repair"
+ (slurp target-path)
+ (lambda (s)
+ (and (str-contains? s "#f")
+ (not (str-contains? s "vector-set!row"))))))
+ (safe-delete-test-file! target-path))
+
+ (let* ([vr-dir "/tmp"]
[target "jcode-verified-existing-full-write-reject.ss"]
[target-path (string-append vr-dir "/" target)]
[initial "(import (jerboa prelude))\n(define (main) (displayln \"ok\"))\n"]