diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/logging.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/logging.rkt index 1096737f33..8a5fbc6cda 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/logging.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/logging.rkt @@ -2,7 +2,16 @@ (require racket/date) -(provide with-logging-to) +(provide with-logging-to + log-counterexample + log-new-avg + log-gen-timeout + log-check-timeout + log-start + log-finished) + +(struct bmark-log-data (data)) +(struct bmark-log-end ()) (define (with-logging-to filename thunk) (define benchmark-logger @@ -17,12 +26,12 @@ (sync (handle-evt body-thd (λ (_) - (log-info "WAIT_FOR") + (log-message (current-logger) 'info "STOP" (bmark-log-end)) (loop))) (handle-evt bmark-log-recv (λ (log-evt) - (cond - [(regexp-match? #rx"WAIT_FOR" (vector-ref log-evt 1)) + (match (vector-ref log-evt 2) + [(bmark-log-end) (void)] [else (handler log-evt) @@ -31,13 +40,68 @@ (define (log-handler recv filename) (λ (log-evt) (define msg (vector-ref log-evt 1)) - (unless (regexp-match? #rx"cm-accomplice" msg) - (call-with-output-file filename - (λ (log-port) - (displayln (string-append (timestamp) " " msg) - log-port)) - #:exists 'append)))) + (define data (vector-ref log-evt 2)) + (match data + [(bmark-log-data data) + (call-with-output-file filename + (λ (log-port) + (write data log-port) + (newline log-port)) + #:exists 'append)] + [_ (void)]))) + +(define (log-counterexample model gen cexp tries time) + (bmark-log 'counterexample + `(#:model ,(path-format model) + #:type ,gen + #:counterexample ,cexp + #:iterations ,tries + #:time ,time))) + +(define (log-new-avg model gen avg dev) + (bmark-log 'new-average + `(#:model ,(path-format model) + #:type ,gen + #:average ,avg + #:stddev ,dev))) + +(define (log-gen-timeout model gen) + (bmark-log 'timeout + `(#:during 'generation + #:model ,(path-format model) + #:type ,gen))) + +(define (log-check-timeout model gen term) + (bmark-log 'timeout + `(#:during 'check + #:term ,term + #:model ,(path-format model) + #:type ,gen))) + +(define (log-start model gen) + (bmark-log 'start + `(#:model ,(path-format model) + #:type ,gen))) + +(define (log-finished model gen time tries countxmps) + (bmark-log 'finished + `(#:model ,(path-format model) + #:type ,gen + #:time-ms ,time + #:attempts ,tries + #:num-counterexamples ,countxmps + #:rate-terms/s ,(exact->inexact (/ tries (/ time 1000))) + #:attempts/cexp ,(if (zero? countxmps) + 'N/A + (exact->inexact (/ tries countxmps)))))) + +(define path-format (compose string->symbol path->string)) + +(define (bmark-log event data) + (log-message (current-logger) 'info "BENCHMARK-LOGGING" + (bmark-log-data `(,event ,(timestamp) ,data)))) + (define (timestamp) (parameterize ([date-display-format 'iso-8601]) - (date->string (current-date) #t))) + (string->symbol (date->string (current-date) #t)))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt index 649b90ad14..9a2e76aabc 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt @@ -144,8 +144,7 @@ [(list tries term) (define continue? (update-results (me-time) fname type verbose?)) (set! counterexamples (add1 counterexamples)) - (log-info (format "~a: counterexample: ~s\n ~s iterations and ~s milliseconds\n" - fname term tries (me-time))) + (log-counterexample fname type term tries (me-time)) (when no-errs? (printf "!---------------------------------------------------!\n") (error 'run-generations "~a: unexpected error on ~s" @@ -164,14 +163,12 @@ (when ((current-process-milliseconds) . > . time-limit) (break (reached-limit tries))) (define term (with-timeout (* 5 1000) generator - (λ () (log-info - (format "\nTimed out generating a test term in: ~a, ~a\n" - fname type)) + (λ () + (log-gen-timeout fname type) (break (timeout))))) (define ok? (with-timeout (* 5 1000) (λ () (check term)) - (λ () (log-info - (format "\nIn ~a, ~a, timed out checking the term: ~s\n" - fname type term)) + (λ () + (log-check-timeout fname type term) (break (timeout))) (λ (exn) (printf "\nException when calling check with:\n~s\n" term) @@ -183,15 +180,14 @@ (loop (add1 tries))])))) (define (exit-message file type terms time countxmps) + (log-finished file type time terms countxmps) (printf "-----------------\n~a, ~s\n" file type) - (print-and-log - (format "Quitting after ~s iterations and ~s milliseconds\n ~s terms/sec\n" - terms time (exact->inexact (/ terms (/ time 1000))))) - (print-and-log - (format "~s counterexamples, ~s tries... ratio: ~s\n" - countxmps terms (if (zero? countxmps) - 'N/A - (exact->inexact (/ terms countxmps))))) + (printf "Quitting after ~s iterations and ~s milliseconds\n ~s terms/sec\n" + terms time (exact->inexact (/ terms (/ time 1000)))) + (printf "~s counterexamples, ~s tries... ratio: ~s\n" + countxmps terms (if (zero? countxmps) + 'N/A + (exact->inexact (/ terms countxmps)))) (printf "-----------------\n")) @@ -201,8 +197,7 @@ (set! stats (hash-set stats type new-stats)) (define avg (statistics-mean new-stats)) (define dev (/ (statistics-stddev new-stats #:bias #t) (sqrt (length (hash-ref results type))))) - (log-info - (format "new average for ~a, ~s: ~s +/- ~s\n" fname type (exact->inexact avg) dev)) + (log-new-avg fname type (exact->inexact avg) dev) (or (= dev 0) ((/ dev avg) . > . 0.1))) @@ -223,6 +218,7 @@ (printf "~a has the error: ~a\n\n" fpath err) (printf "Running ~a....\n" fpath) (printf "Using generator: ~s\n" gen-type) + (log-start fpath gen-type) (cond [(equal? gen-type 'fixed) (define small-counter-example