Focus verified post-failure repairs
ober
b85c06de12889bfc68673bcb83f0f8f77c130a8c
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -217,13 +217,19 @@ (> (current-successful-edit-count) 0)))) (def (verified-provider-tool-spec spec) - (if (and (local-focused-repair-mode?) - (not (current-pending-ss-create-repair)) - (string=? (tool-spec-name spec) "edit")) - (make-tool-spec "edit" - "Replace exact existing text only. args: {\"path\": string, \"old_str\": string, \"new_str\": string}. Full-file rewrites are disabled after a valid local artifact exists; use line_edit, replace_def, or replace_range for bounded repairs." - *exact-edit-schema*) - spec)) + (cond + ((and (current-after-failed-verify?) + (string=? (tool-spec-name spec) "read")) + (make-tool-spec "read" + "Read the verifier-implicated source file. After verify failure, prefer the writable source path and a narrow line range; do not inspect dependency caches for ordinary source errors." + (scoped-read-schema))) + ((and (local-focused-repair-mode?) + (not (current-pending-ss-create-repair)) + (string=? (tool-spec-name spec) "edit")) + (make-tool-spec "edit" + "Replace exact existing text only. args: {\"path\": string, \"old_str\": string, \"new_str\": string}. Full-file rewrites are disabled after a valid local artifact exists; use line_edit, replace_def, or replace_range for bounded repairs." + *exact-edit-schema*)) + (else spec))) (def (verified-post-edit-tool-spec? spec) (member (tool-spec-name spec) @@ -275,6 +281,12 @@ ((and (current-edited-since-verify?) (not (verified-post-edit-tool-spec? spec))) #f) + ;; After the verifier fails, list/navigation tends to send weaker + ;; models into dependency caches instead of the implicated source. + ;; Keep read/balance for targeted source inspection. + ((and (current-after-failed-verify?) + (verified-navigation-tool-spec? spec)) + #f) ;; Shell aliases are inspection aids, not an alternate verifier. ;; Stop advertising them once their pre-edit allowance is spent or ;; while a successful edit is waiting for the authoritative verify. @@ -859,6 +871,65 @@ path line-no line-no line-no 'unbound-symbol candidate)))))) +(def racket-style-iteration-patterns + '("(for (" "(for/list" "(for/vector" "(in-range")) + +(def (first-pattern-index content patterns) + (let loop ((rest patterns) (best #f) (best-pattern #f)) + (cond + ((null? rest) (and best (cons best best-pattern))) + (else + (let ((idx (string-contains content (car rest)))) + (if (and idx (or (not best) (< idx best))) + (loop (cdr rest) idx (car rest)) + (loop (cdr rest) best best-pattern))))))) + +(def (source-racket-style-iteration-match cwd path symbol) + (and (source-ss-path? path) + (file-exists? (abs-path cwd path)) + (not (file-directory? (abs-path cwd path))) + (let* ((content (read-file-string (abs-path cwd path))) + (match (first-pattern-index + content racket-style-iteration-patterns))) + (and match + (string-contains content symbol) + (list path content (car match) (cdr match)))))) + +(def (source-containing-racket-style-iteration cwd symbol) + (let ((preferred (scope-primary-file (current-write-scope)))) + (or (and preferred + (source-racket-style-iteration-match cwd preferred symbol)) + (let loop ((entries (directory-list cwd))) + (cond + ((null? entries) #f) + (else + (or (source-racket-style-iteration-match + cwd (car entries) symbol) + (loop (cdr entries))))))))) + +(def (unsupported-iteration-diagnosis detail cwd) + (let ((symbol (unbound-variable-name detail))) + (and symbol + (let ((source (source-containing-racket-style-iteration cwd symbol))) + (and source + (let* ((path (car source)) + (content (cadr source)) + (index (caddr source)) + (pattern (cadddr source)) + (line-no (line-number-at-index content index)) + (line (line-at (string-split content #\newline) line-no))) + (string-append + "\n\nJerboa iteration diagnosis: the verifier reported `" + symbol + "` is unbound while the source uses Racket-style iteration forms such as `for`, `for/list`, `for/vector`, or `in-range`. These forms are not portable in verified Jerboa scripts and may not bind loop variables here. Replace the implicated iteration with named-let recursion, `do`, or explicit list/vector construction, then call verify. Do not inspect dependency caches for this failure.\n" + "Iteration source target: " + path ":" (number->string line-no) + " contains `" pattern "`" + (if line + (string-append "\n" (number->string line-no) + ": " line) + "")))))))) + (def (runtime-procedure-name detail) (let ((marker "#<procedure ") (suffix " at ")) @@ -1350,6 +1421,7 @@ (empty-body-diagnosis detail cwd) (invalid-syntax-diagnosis detail cwd) (call-arity-diagnosis detail cwd) + (unsupported-iteration-diagnosis detail cwd) (unbound-symbol-diagnosis detail cwd) (runtime-call-arity-diagnosis detail cwd) (qt-lifecycle-diagnosis detail cwd) @@ -5364,6 +5436,21 @@ (cons "limit" (number-schema "Maximum characters to return"))))) (cons "required" (list "path"))))) +(def (scoped-read-schema) + (schema-object + (list (cons "type" "object") + (cons "properties" + (schema-object + (list (cons "path" + (mutation-path-schema + "Source file path to read after verify failure")) + (cons "line" (number-schema "1-based line number to start at")) + (cons "start" (number-schema "1-based start line")) + (cons "end" (number-schema "1-based end line")) + (cons "offset" (number-schema "Character offset")) + (cons "limit" (number-schema "Maximum characters to return"))))) + (cons "required" (list "path"))))) + (def *line-read-schema* (schema-object (list (cons "type" "object") @@ -5989,6 +6076,7 @@ "" (string-append expert-guidance "\n"))) "Jerboa binding rule: use def/define only for top-level declarations. Inside procedure, let, cond, and let-values bodies, bind locals with let, let*, named let, or existing returned variables; an internal def/define is an invalid context for definition even if an example suggests it.\n" + "Jerboa iteration rule: avoid Racket-style `for`, `for/list`, `for/vector`, and `in-range` unless the repository proves those exact forms work. Use named let recursion, `do`, or explicit list/vector builders so loop variables are ordinary lexical bindings.\n" "Workflow:\n" "1. read any files you need to understand first.\n" "2. edit to write or change code. Prefer deterministic, bounded targets: one complete file for a new script, one whole function with replace_def, one diagnosed span with replace_range, or one known line with line_edit. For existing .ss files, prefer local edits over full-file rewrites.\n" --- a/test/run.ss +++ b/test/run.ss @@ -5772,6 +5772,130 @@ broad-hidden? #t)) (safe-delete-test-file! target-path)) +(let* ([vr-dir "/tmp"] + [target "jcode-verified-post-failure-read-scope.ss"] + [target-path (string-append vr-dir "/" target)] + [list-hidden? #f] + [read-scoped? #f] + [resp + (lambda (_messages specs step) + (case step + [(0) (list (make-wtool-call "verify" '() #f))] + [(1) + (let* ([names (map tool-spec-name specs)] + [read-spec + (let loop ([xs specs]) + (cond + [(null? xs) #f] + [(string=? (tool-spec-name (car xs)) "read") + (car xs)] + [else (loop (cdr xs))]))]) + (set! list-hidden? (not (member "list" names))) + (set! read-scoped? + (and read-spec + (let* ([schema (tool-spec-parameters read-spec)] + [props (hashtable-ref schema "properties" #f)] + [path-prop (and props + (hashtable-ref props "path" #f))] + [enum (and path-prop + (hashtable-ref path-prop "enum" #f))]) + (and enum (equal? enum (list target))))))) + (list (make-wtool-call + "write" + (list (cons "path" target) + (cons "content" "fixed\n")) + #f))] + [(2) (list (make-wtool-call "verify" '() #f))] + [else (error 'test "unexpected post-failure read scope step")]))]) + (safe-delete-test-file! target-path) + (write-test-output-file target-path + (lambda (o) (display "broken\n" o)) + 'replace) + (let ([result + (verified-run + resp + "scope post-failure source reads" + (list (cons 'cwd vr-dir) + (cons 'verify-command + (string-append "grep -q fixed " target)) + (cons 'write-scope (parse-write-scope target)) + (cons 'max-iterations 8)))]) + (check-pred! "verified-run: scoped post-failure read run verifies" + result + (lambda (s) (str-contains? s "VERIFIED: exit 0"))) + (check! "verified-run: post-failure list schema hidden" + list-hidden? #t) + (check! "verified-run: post-failure read schema scoped" + read-scoped? #t)) + (safe-delete-test-file! target-path)) + +(let* ([vr-dir "/tmp"] + [target "jcode-verified-unsupported-for.ss"] + [target-path (string-append vr-dir "/" target)] + [tool-results '()] + [initial + (string-append + "(import (jerboa prelude))\n" + "(def (main)\n" + " (for ([i (in-range 3)])\n" + " (display i)))\n" + "(main)\n")] + [fixed + (string-append + "(import (jerboa prelude))\n" + "(def (main)\n" + " (let loop ([i 0])\n" + " (when (< i 3)\n" + " (display i)\n" + " (loop (+ i 1)))))\n" + "(main)\n")] + [resp + (lambda (_messages _specs step) + (case step + [(0) (list (make-wtool-call "verify" '() #f))] + [(1) + (list (make-wtool-call + "edit" + (list (cons "path" target) + (cons "content" fixed)) + #f))] + [(2) (list (make-wtool-call "verify" '() #f))] + [else (error 'test "unexpected unsupported for step")]))]) + (safe-delete-test-file! target-path) + (write-test-output-file target-path + (lambda (o) (display initial o)) + 'replace) + (let ([result + (verified-run + resp + "repair unsupported Jerboa for iteration" + (list (cons 'cwd vr-dir) + (cons 'verify-command + (string-append + "if grep -q '(for' " target + "; then echo 'Exception: variable i is not bound'; exit 1; fi")) + (cons 'write-scope (parse-write-scope target)) + (cons 'max-iterations 8) + (cons 'on-message + (lambda (m) + (when (equal? (message-role m) "tool") + (set! tool-results + (cons (message-content m) tool-results)))))))]) + (check! "verified-run: unsupported for repair verifies" + result "VERIFIED: exit 0\n") + (check-pred! "verified-run: unsupported for diagnosis explains loop rewrite" + (reverse tool-results) + (lambda (xs) + (let loop ([ys xs]) + (cond + [(null? ys) #f] + [(and (str-contains? (car ys) "Jerboa iteration diagnosis") + (str-contains? (car ys) "for/list") + (str-contains? (car ys) "named-let recursion") + (str-contains? (car ys) target)) #t] + [else (loop (cdr ys))]))))) + (safe-delete-test-file! target-path)) + (let* ([failure-before fake-mcp-failure-calls] [error-fix-before fake-mcp-error-fix-calls] [anti-pattern-before fake-mcp-anti-pattern-calls]