Hide broad writes after repeated draft rejects
ober
06e0fbaf313c5c042f9e265e283d340a5ed74e96
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -305,7 +305,9 @@ ;; repo/API inspection keeps models away from the absent target. ((and (current-pending-ss-create-repair) (current-rejected-ss-draft) - (not (verified-current-create-draft-tool-spec? spec))) + (not (if (rejected-draft-staged-repair-mode?) + (verified-staged-repair-tool-spec? spec) + (verified-current-create-draft-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/test/run.ss +++ b/test/run.ss @@ -3976,8 +3976,8 @@ (and (member "line_edit" names) (member "replace_def" names) (member "replace_range" names) - (member "edit" names) - (member "write" names) + (not (member "edit" names)) + (not (member "write" names)) (member "read" names) (member "balance" names) (not (member "verify" names)) @@ -4730,8 +4730,8 @@ (cons 'max-iterations 8)))]) (check! "verified-run: repeated rejected draft schema repair verifies" result "VERIFIED: exit 0\n")) - (check-pred! "verified-run: repeated syntax draft keeps write schema" - tool-names-after-repeat (lambda (names) (member "write" names))) + (check-pred! "verified-run: repeated syntax draft hides write schema" + tool-names-after-repeat (lambda (names) (not (member "write" names)))) (check-pred! "verified-run: repeated rejected draft keeps line edit schema" tool-names-after-repeat (lambda (names) (member "line_edit" names))) (safe-delete-test-file! target-path)) @@ -4841,10 +4841,10 @@ (cons 'max-iterations 8)))]) (check! "verified-run: missing create staged repair after rejects verifies" result "VERIFIED: exit 0\n")) - (check-pred! "verified-run: missing create staged repair keeps write" - tool-names-after-repeat (lambda (names) (member "write" names))) - (check-pred! "verified-run: missing create staged repair keeps edit" - tool-names-after-repeat (lambda (names) (member "edit" names))) + (check-pred! "verified-run: missing create staged repair hides write" + tool-names-after-repeat (lambda (names) (not (member "write" names)))) + (check-pred! "verified-run: missing create staged repair hides edit" + tool-names-after-repeat (lambda (names) (not (member "edit" names)))) (check-pred! "verified-run: missing create staged range reaches disk" (call-with-input-file target-path (lambda (p) (get-string-all p))) (lambda (s) (str-contains? s "fixed"))) @@ -8930,6 +8930,63 @@ (safe-delete-test-file! target-path)) (let* ([vr-dir "/tmp"] + [target "jcode-verified-repeated-syntax-create-bounded.ss"] + [target-path (string-append vr-dir "/" target)] + [broken1 "(import (jerboa prelude))\n(def (main)\n (return 1))\n(main)\n"] + [broken2 "(import (jerboa prelude))\n(def (main)\n (return 2))\n(main)\n"] + [fixed "(import (jerboa prelude))\n(def (main)\n (displayln \"fixed\"))\n(main)\n"] + [tool-names-after-repeat '()] + [i 0] + [slurp (lambda (p) (call-with-input-file p (lambda (in) (get-string-all in))))]) + (safe-delete-test-file! target-path) + (let* ([scope (parse-write-scope target)] + [provider + (lambda (_messages tool-specs _step) + (set! i (+ i 1)) + (when (= i 3) + (set! tool-names-after-repeat + (map tool-spec-name tool-specs))) + (cond + [(= i 1) + (list (make-wtool-call "write" + (list (cons "path" target) + (cons "content" broken1)) #f))] + [(= i 2) + (list (make-wtool-call "write" + (list (cons "path" target) + (cons "content" broken2)) #f))] + [(= i 3) + (list (make-wtool-call "replace_range" + (list (cons "path" target) + (cons "start" 1) + (cons "end" 4) + (cons "content" fixed)) #f))] + [else + (list (make-wtool-call "done" + '(("summary" . "repeated-syntax-create-bounded-ok")) #f))]))] + [result (verified-run provider + "hide broad writes after repeated syntax-broken missing create" + (list (cons 'cwd vr-dir) + (cons 'verify-command + (string-append "grep -q fixed " target)) + (cons 'write-scope scope) + (cons 'local-model? #t) + (cons 'max-iterations 8) + (cons 'max-tool-errors 4)))]) + (check! "verified-run: repeated syntax create bounded repair recovers" + result "VERIFIED: exit 0\n") + (check! "verified-run: repeated syntax create writes repaired file" + (slurp target-path) (string-append fixed "\n")) + (check-pred! "verified-run: repeated syntax create hides broad write" + tool-names-after-repeat + (lambda (names) + (and (member "line_edit" names) + (member "replace_range" names) + (not (member "edit" names)) + (not (member "write" names)))))) + (safe-delete-test-file! target-path)) + + (let* ([vr-dir "/tmp"] [target "jcode-verified-replace-range.ss"] [target-path (string-append vr-dir "/" target)] [initial "(import (jerboa prelude))\n(define (bad)\n (displayln \"bad\")\n\n(define (ok) 1)\n"]