Focus verified repair schemas
ober
286167d62baa446d69c4e9b57054ddaf5176ef83
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -193,6 +193,10 @@ (member (tool-spec-name spec) '("edit" "write" "line_edit" "replace_def" "replace_range" "verify"))) +(def (verified-missing-create-repair-tool-spec? spec) + (member (tool-spec-name spec) + '("edit" "write" "line_edit" "replace_def" "replace_range"))) + (def (verified-rejected-draft-inspection-tool-spec? spec) (member (tool-spec-name spec) '("read" "balance"))) @@ -257,6 +261,13 @@ (not (current-pending-ss-create-repair)) (string=? name "write")) #f) + ;; If a missing .ss create produced a rejected draft, the next + ;; useful action is to repair or replace that staged draft. Further + ;; repo/API inspection keeps models away from the absent target. + ((and (current-pending-ss-create-repair) + (current-rejected-ss-draft) + (not (verified-missing-create-repair-tool-spec? spec))) + #f) ;; After a successful edit, another observation should come from the ;; authoritative verifier. Keep repair tools in case the model spots ;; a mistake, but remove inspection, discovery, scaffold, and done. @@ -274,6 +285,14 @@ #f) ;; Keep cheap directory navigation separate from source inspection, ;; so locating an approved dependency does not consume every read. + ((and (current-verified-local-model?) + (= (current-successful-edit-count) 0) + (not (current-rejected-ss-draft)) + (not (current-pending-ss-create-repair)) + (>= (pre-edit-inspection-total) + local-force-first-edit-inspection-count) + (verified-inspection-tool-spec? spec)) + #f) ((and (= (current-successful-edit-count) 0) (not (current-rejected-ss-draft)) (not (current-pending-ss-create-repair)) @@ -360,6 +379,7 @@ (def remote-pre-edit-inspection-limit 12) (def remote-pre-edit-navigation-limit 10) (def remote-force-first-edit-inspection-count 10) +(def local-force-first-edit-inspection-count 5) (def (pre-edit-inspection-total) (+ (current-pre-edit-inspection-count) @@ -374,8 +394,8 @@ (not (current-rejected-ss-draft)) (not (current-pending-ss-create-repair)) (if (current-verified-local-model?) - (>= (current-pre-edit-inspection-count) - local-pre-edit-inspection-limit) + (>= (pre-edit-inspection-total) + local-force-first-edit-inspection-count) (>= (pre-edit-inspection-total) remote-force-first-edit-inspection-count)) (tool-specs-include? specs "edit") --- a/test/run.ss +++ b/test/run.ss @@ -3405,6 +3405,68 @@ [else (loop (cdr ys))]))))) (safe-delete-test-file! target-path)) + (let* ([vr-dir "/tmp/jcode-verified-local-force-schema"] + [target "local-force-schema.txt"] + [target-path (string-append vr-dir "/" target)] + [test-dir (string-append vr-dir "/test")] + [makefile (string-append vr-dir "/Makefile")] + [runner (string-append test-dir "/run-tests.sh")] + [seen-specs '()] + [i 0] + [provider + (lambda (_messages tool-specs _step) + (set! seen-specs + (cons (map tool-spec-name tool-specs) seen-specs)) + (set! i (+ i 1)) + (cond + [(= i 1) + (list (make-wtool-call "list" '(("path" . ".")) #f))] + [(= i 2) + (list (make-wtool-call "read" '(("path" . "Makefile")) #f))] + [(= i 3) + (list (make-wtool-call "list" '(("path" . "test")) #f))] + [(= i 4) + (list (make-wtool-call "read" '(("path" . "test/run-tests.sh")) #f))] + [(= i 5) + (list (make-wtool-call "list" '(("path" . ".")) #f))] + [else + (list (make-wtool-call "edit" + (list (cons "path" target) + (cons "content" "fixed\n")) #f))]))]) + (ensure-test-directory! vr-dir) + (ensure-test-directory! test-dir) + (safe-delete-test-file! target-path) + (write-test-output-file makefile + (lambda (o) (display ".PHONY: test\n" o)) 'replace) + (write-test-output-file runner + (lambda (o) (display "#!/usr/bin/env bash\n" o)) 'replace) + (let ([result + (verified-run (provider-responder provider) + "hide local inspection schemas after combined pressure" + (list + (cons 'cwd vr-dir) + (cons 'verify-command + (string-append "grep -q fixed " target)) + (cons 'write-scope (parse-write-scope target)) + (cons 'local-model? #t) + (cons 'max-iterations 8) + (cons 'max-tool-errors 0)))]) + (check! "verified-run: local combined inspection pressure still verifies" + result "VERIFIED: exit 0\n") + (check-pred! "verified-run: local combined pressure hides inspection schemas" + (reverse seen-specs) + (lambda (xs) + (and (>= (length xs) 6) + (let ([names (list-ref xs 5)]) + (and (member "edit" names) + (member "write" names) + (not (member "read" names)) + (not (member "list" names)) + (not (member "balance" names)))))))) + (safe-delete-test-file! target-path) + (safe-delete-test-file! makefile) + (safe-delete-test-file! runner)) + (let* ([vr-dir "/tmp"] [target "jcode-verified-local-navigation-budget.txt"] [target-path (string-append vr-dir "/" target)] @@ -3564,7 +3626,7 @@ (member "line_edit" names) (member "replace_def" names) (member "replace_range" names) - (member "verify" names) + (not (member "verify" names)) (not (member "read" names)) (not (member "balance" names))))) (check! "verified-run: local staged line edit promotes repaired file" @@ -7360,6 +7422,59 @@ "Jerboa compatibility alias repair"))))) (safe-delete-test-file! target-path)) +(let* ([vr-dir "/tmp"] + [target "jcode-verified-missing-create-schema.ss"] + [target-path (string-append vr-dir "/" target)] + [bad "(import (jerboa prelude))\n(define (main)\n (displayln \"bad\")))\n"] + [good "(import (jerboa prelude))\n(define (main)\n (displayln \"fixed\"))\n(main)\n"] + [seen-specs '()] + [i 0] + [provider + (lambda (_messages tool-specs _step) + (set! seen-specs + (cons (map tool-spec-name tool-specs) seen-specs)) + (set! i (+ i 1)) + (cond + [(= i 1) + (list (make-wtool-call "edit" + (list (cons "path" target) + (cons "content" bad)) #f))] + [(= i 2) + (list (make-wtool-call "edit" + (list (cons "path" target) + (cons "content" good)) #f))] + [(= i 3) + (list (make-wtool-call "verify" '() #f))] + [else + (list (make-wtool-call "done" + '(("summary" . "missing-create-schema-ok")) #f))]))]) + (safe-delete-test-file! target-path) + (let* ([scope (parse-write-scope target)] + [wf (coding-workflow + (string-append "grep -q fixed " target) + vr-dir + (list (cons 'write-scope scope)))] + [result (parameterize ((current-write-scope scope)) + (run-workflow wf "hide reads after missing create rejection" + (provider-responder provider) + (list (cons 'max-iterations 8) + (cons 'max-tool-errors 3))))]) + (check! "verified-run: missing create schema repair reaches done" + result "missing-create-schema-ok") + (check-pred! "verified-run: missing create repair hides inspection schemas" + (reverse seen-specs) + (lambda (xs) + (and (>= (length xs) 2) + (let ([names (list-ref xs 1)]) + (and (member "edit" names) + (member "write" names) + (member "line_edit" names) + (not (member "read" names)) + (not (member "list" names)) + (not (member "balance" names)) + (not (member "verify" names)))))))) + (safe-delete-test-file! target-path)) + (let* ([vr-dir "/tmp"] [target "jcode-verified-replace-range.ss"] [target-path (string-append vr-dir "/" target)]