Allow recovery read after rejected range repair
ober
3443891dfc6cac832b4823c5875ef172f18081b1
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -2381,6 +2381,9 @@ (def current-required-repair-inspections (make-parameter 0)) +(def current-required-repair-recovery-read-path + (make-parameter #f)) + (def (reset-verified-attempt-state!) (current-pending-ss-create-repair #f) (current-rejected-ss-draft #f) @@ -2414,7 +2417,8 @@ (current-force-expert-next? #f) (current-last-verify-detail #f) (current-required-range-repair #f) - (current-required-repair-inspections 0)) + (current-required-repair-inspections 0) + (current-required-repair-recovery-read-path #f)) (def inspection-after-failed-verify-limit 6) @@ -2630,7 +2634,8 @@ (current-inspections-after-failed-verify 0) (current-last-verify-detail #f) (current-required-range-repair #f) - (current-required-repair-inspections 0)) + (current-required-repair-inspections 0) + (current-required-repair-recovery-read-path #f)) (def (record-verify-result! result . review-after-verify) (let ((passed? (and (pair? result) (car result))) @@ -2786,11 +2791,21 @@ (and (<= start (repair-ref repair 'start)) (>= end (repair-ref repair 'end))))))) +(def (consume-required-repair-recovery-read? cwd path repair) + (let ((allowed (current-required-repair-recovery-read-path))) + (and allowed + (repair-path-matches? cwd repair path) + (same-verified-path? cwd allowed path) + (begin + (current-required-repair-recovery-read-path #f) + #t)))) + (def (required-repair-read-block-message cwd args) (let ((repair (current-required-range-repair))) (and repair (let ((path (arg-path args #f))) (and (not (rejected-draft-content cwd path)) + (not (consume-required-repair-recovery-read? cwd path repair)) (not (and (repair-path-matches? cwd repair path) (read-covers-required-repair? args repair))) (let ((inspection-count (note-required-repair-inspection!))) @@ -2988,11 +3003,14 @@ (repair-ref repair 'end)))) (string-append msg - (if (current-verified-local-model?) - "\nThe file was not written. Structural repair is still pending. Retry with a span that leaves the complete file syntax-correct, or use edit/write with a syntax-correct complete file when this span exposes a second structural error. " - "\nThe file was not written. Structural repair is still pending; do not switch to edit or a full-file rewrite. ") - (range-repair-instruction repair) - (best-repair-candidate-text cwd repair label))) + (string-append + "\nThe file was not written. Structural repair is still pending. " + "One same-file recovery read is available if the rejected draft exposed an off-span balance error; use read(path=\"" + path + "\") or the exact span read below, then retry with a span that leaves the complete file syntax-correct. " + "Use edit/write with a syntax-correct complete file only when this span exposes a second structural error. ") + (range-repair-instruction repair) + (best-repair-candidate-text cwd repair label))) (string-append msg "\n" (ss-repair-instruction path))))) (def (same-verified-path? cwd a b) @@ -5464,6 +5482,14 @@ ;; rejected replacement draft tends to send weak models into unrelated ;; full-file rewrites. (reset-rejected-draft-state!) + (when (and (repair-path-matches? cwd repair path) + (replace-range-overlaps-required-repair? + cwd + (list (cons "path" path) + (cons "start" start-line) + (cons "end" end-line)) + repair)) + (current-required-repair-recovery-read-path path)) (raise-recoverable-tool-error (structural-repair-rejection-message cwd path msg) 'replace_range)) @@ -6571,6 +6597,7 @@ (if pending (cons #f pending) (let ((result (run-verify-command verify-cmd cwd))) + (current-required-repair-recovery-read-path #f) (current-required-range-repair (and (pair? result) (not (car result)) @@ -7021,6 +7048,7 @@ (current-last-verify-detail #f) (current-required-range-repair #f) (current-required-repair-inspections 0) + (current-required-repair-recovery-read-path #f) (current-unknown-tool-recovery (lambda (name available) (staged-create-hidden-write-message --- a/test/run.ss +++ b/test/run.ss @@ -7421,6 +7421,91 @@ (str-contains? (list-ref xs 5) "Structural repair required"))))) (safe-delete-test-file! target-path)) + (let* ([vr-dir "/tmp"] + [target "jcode-invalid-syntax-read-after-range-reject.ss"] + [target-path (string-append vr-dir "/" target)] + [bad-source "(import (jerboa prelude))\n(define (render)\n (let ((r g b)\n (call-with-values (lambda () (values 1 2 3))\n (lambda (r g b) (displayln r)))))\n(define (next) 2)\n"] + [bad-span "(define (render)\n (displayln \"fixed\")))"] + [fixed-span "(define (render)\n (displayln \"fixed\"))"] + [verify-cmd (string-append + "if grep -q fixed " + target + "; then true; else printf '%s\\n' 'Exception: invalid syntax (let ((r g b) (call-with-values (...) (...)))) at line 3, char 3 of " + target + "' >&2; exit 255; fi")] + [tool-results '()] + [resp (scripted-responder + (list + (list (make-wtool-call "verify" '() #f)) + (list + (make-wtool-call + "replace_range" + (list (cons "path" target) + (cons "start" 2) + (cons "end" 4) + (cons "content" bad-span)) + #f)) + (list + (make-wtool-call + "read" + (list (cons "path" target)) + #f)) + (list + (make-wtool-call + "replace_range" + (list (cons "path" target) + (cons "start" 2) + (cons "end" 4) + (cons "content" fixed-span)) + #f)) + (list (make-wtool-call "verify" '() #f)) + (list (make-wtool-call "done" '(("summary" . "invalid-syntax-read-after-range-reject-ok")) #f))))] + [wf (coding-workflow verify-cmd vr-dir + (list (cons 'run-aliases? #t)))]) + (safe-delete-test-file! target-path) + (write-test-output-file target-path + (lambda (o) (display bad-source o)) + 'replace) + (let ([result (run-workflow wf "same-file read after rejected required range repair" 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: rejected required range repair read recovers" + result "invalid-syntax-read-after-range-reject-ok") + (check-pred! "verified-run: rejected required range repair advertises recovery read" + (reverse tool-results) + (lambda (xs) + (let loop ([ys xs]) + (cond + [(null? ys) #f] + [(and (str-contains? (car ys) "One same-file recovery read is available") + (str-contains? (car ys) "read(path=\"") + (str-contains? (car ys) "Structural repair required")) + #t] + [else (loop (cdr ys))])))) + (check-pred! "verified-run: pending repair read after range reject is allowed" + (reverse tool-results) + (lambda (xs) + (let loop ([ys xs] [saw-reject #f]) + (cond + [(null? ys) #f] + [(and saw-reject + (str-contains? (car ys) "(define (next) 2)") + (not (str-contains? (car ys) + "A structural verifier diagnosis is pending"))) + #t] + [else + (loop (cdr ys) + (or saw-reject + (str-contains? (car ys) + "One same-file recovery read is available")))]))))) + (safe-delete-test-file! target-path)) + (for-each (lambda (case) (let* ([label (car case)]