Allow substantial complete Jerboa rewrites
ober
069b7f9702a78a6dc480f7cc5ec0e67e0a66d483
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -5057,6 +5057,7 @@ (def meaningful-source-bytes-threshold 1000) (def tiny-rewrite-bytes-threshold 500) +(def substantial-complete-source-rewrite-bytes-threshold 8192) (def (meaningful-source-file? path content) (and (source-ss-path? path) @@ -5065,6 +5066,17 @@ (string-contains content "(define ") (string-contains content "(lambda")))) +(def (substantial-complete-source-rewrite? path content) + (and (source-ss-path? path) + (>= (string-length content) + substantial-complete-source-rewrite-bytes-threshold) + (looks-like-complete-file? content) + (ss-create-has-substantive-form? content) + (or (string-contains content "--self-test") + (string-contains content "with-qt-app") + (string-contains content "(def (main") + (string-contains content "(define (main")))) + (def (diagnostic-stub-content? content) (let ((s (string-downcase (string-trim content)))) (or (< (string-length s) tiny-rewrite-bytes-threshold) @@ -5095,6 +5107,7 @@ (and (current-after-failed-verify?) (meaningful-source-file? path old-content) (looks-like-complete-file? new-content) + (not (substantial-complete-source-rewrite? path new-content)) (< (string-length new-content) (quotient (* (string-length old-content) 4) 5)) (string-append --- a/test/run.ss +++ b/test/run.ss @@ -11509,6 +11509,69 @@ (safe-delete-test-file! target-path)) (let* ([vr-dir "/tmp"] + [target "jcode-verified-substantial-complete-rewrite.ss"] + [target-path (string-append vr-dir "/" target)] + [initial (string-append + "(import (jerboa prelude))\n\n" + "(def old-filler \"" + (make-string 15000 #\x) + "\")\n\n" + "(def (main argv)\n" + " (displayln \"old\"))\n")] + [replacement (string-append + "(import (jerboa prelude))\n\n" + "(def new-filler \"" + (make-string 8500 #\y) + "\")\n\n" + "(def (main argv)\n" + " (if (member \"--self-test\" argv)\n" + " (displayln \"PASS\")\n" + " (with-qt-app app\n" + " (displayln \"PASS\"))))\n")] + [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 PASS " target) vr-dir + (list (cons 'write-scope scope)))] + [resp (scripted-responder + (list + (list (make-wtool-call "verify" '() #f)) + (list + (make-wtool-call + "edit" + (list (cons "path" target) + (cons "content" replacement)) + #f)) + (list (make-wtool-call "verify" '() #f)) + (list (make-wtool-call "done" '(("summary" . "substantial-complete-rewrite")) #f))))] + [result (parameterize ((current-write-scope scope)) + (run-workflow wf "accept substantial complete rewrite after verify failure" resp + (list (cons 'max-iterations 8) + (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: substantial complete rewrite reaches verified done" + result "substantial-complete-rewrite") + (check! "verified-run: substantial complete rewrite is written" + (slurp target-path) replacement) + (check-pred! "verified-run: substantial complete rewrite avoids truncation refusal" + (reverse tool-results) + (lambda (xs) + (let loop ([ys xs]) + (cond + [(null? ys) #t] + [(str-contains? (car ys) "probably a completion-truncated prefix") #f] + [else (loop (cdr ys))]))))) + (safe-delete-test-file! target-path)) + + (let* ([vr-dir "/tmp"] [target "jcode-verified-existing-full-write-lock.ss"] [target-path (string-append vr-dir "/" target)] [initial "(import (jerboa prelude))\n(define (main)\n (display \"ok\")\n (newline))\n(main)"]