report.rkt

#lang racket

(require racket/path racket/set racket/engine racket/cmdline)
(require json (only-in xml write-xexpr))
(require "common.rkt" "input.rkt" "frontend.rkt" "dom.rkt" "tree.rkt" "proofs.rkt" "assertions.rkt" "smt.rkt")

(define verbose (make-parameter false))
(define timeout (make-parameter 60))
(define show-success (make-parameter false))
(define expected-failures (make-parameter '()))

(define (expected? . info)
  (set-member? (expected-failures) info))

(define (dom-not-something d)
  (match-define (dom name ctx elts boxes _) d)
  
  (define constraints 0)

  (let loop ([tree boxes])
    (when (member (caar tree) '(LINE BLOCK INLINE))
      (set! constraints (+ constraints (count (curryr member '(:x :y :w :h)) (cdar tree)))))
    (for-each loop (cdr tree)))
  
  (define idx (random 0 constraints))
  (set! constraints 0)

  ;; Not my fault
  (struct-copy dom d
               [boxes
                (let loop ([tree boxes])
                  (cond
                   [(> constraints idx) tree]
                   [(member (caar tree) '(LINE BLOCK INLINE))
                    (set! constraints (+ constraints (count (curryr member '(:x :y :w :h)) (cdar tree))))
                    (cons (cons (caar tree)
                                (let loop2 ([n (- constraints idx)] [props (cdar tree)])
                                  (cond
                                   [(null? props) props]
                                   [(and (= n 1) (member (car props) '(:x :y :w :h)))
                                    (list* (car props) `(not ,(cadr props)) (cddr props))]
                                   [(and (member (car props) '(:x :y :w :h)))
                                    (list* (car props) (cadr props) (loop2 (- n 1) (cddr props)))]
                                   [else
                                    (list* (car props) (cadr props) (loop2 n (cddr props)))])))
                          (map loop (cdr tree)))]
                   [else (cons (car tree) (map loop (cdr tree)))]))]))

(define (section->tuple s)
  (if (string=? (substring s 0 1) "s")
      (cons "s" (map (λ (c) (or (string->number c) c)) (string-split (substring s 1) ".")))
      '("u")))

(define (number-string<? c1 c2)
  (cond
   [(and (number? c1) (number? c2)) (< c1 c2)]
   [(number? c1) #t]
   [(number? c2) #f]
   [else (string<? c1 c2)]))

(define (section-tuple<? s1 s2)
  (cond
   [(and (null? s1) (null? s2)) #f]
   [(null? s1) #t]
   [(null? s2) #f]
   [(number-string<? (car s1) (car s2)) #t]
   [(number-string<? (car s2) (car s1)) #f]
   [else (section-tuple<? (cdr s1) (cdr s2))]))

(define (section<? s1 s2)
  (section-tuple<? (section->tuple s1) (section->tuple s2)))

(define (if-verbose port)
  (if (verbose) port (open-output-nowhere)))

(define (run-problem prob #:fuzz [fuzz? '(/ 10 60)])
  (define custodian (make-custodian))
  (define eng
    (engine (λ (_)
                (parameterize ([current-error-port (if-verbose (current-error-port))]
                               [current-output-port (if-verbose (current-output-port))]
                               [current-subprocess-custodian-mode 'kill]
                               [current-custodian custodian]
                               [*fuzz* fuzz?])
                  (solve-problem prob)))))

  (define t (current-inexact-milliseconds))
  (define res (if (engine-run (* 1000 (timeout)) eng) (engine-result eng) 'timeout))
  (define runtime (- (current-inexact-milliseconds) t))

  (match res [(list 'error e) ((error-display-handler) (exn-message e) e)] [_ (void)])

  (engine-kill eng)
  (custodian-shutdown-all custodian)
  (values res runtime))

(struct result (file problem subproblem test section status description features time url) #:prefab)

(define (make-result file pname prob #:subproblem [subproblem #f] #:index [index (hash)])
  (define url (car (dict-ref prob ':url '("/tmp"))))
  (result file pname subproblem
          (file-name-stem url) (get-index index (file-name-stem url))
          'ready (car (dict-ref prob ':title))
          (dict-ref prob ':features '()) #f url))

(define (get-status info prob res #:invert [invert? #f] #:unsupported [unsupported? #t])
  (define out
    (match res
      ['timeout 'timeout]
      [(list 'error e) 'error]
      ['break 'break]
      [(success doms test) (if invert? 'fail 'success)]
      [(failure doms) (if invert? 'success 'fail)]))
  (cond
   [(not (equal? out 'fail))
    out]
   [(apply expected? info)
    'expected]
   [(and
     (not (subset? (dict-ref prob ':features '()) (supported-features)))
     unsupported?)
    'unsupported]
   [else
    'fail]))

(define (test-regression file pname prob #:index [index (hash)])
  (eprintf "~a\t~a\t" file pname)
  (define res (make-result file pname prob #:index index))
  (define-values (out runtime) (run-problem prob))
  (define status (get-status (list file pname) prob out #:invert false #:unsupported true))
  (eprintf "~a\n" status)
  (flush-output (current-error-port))
  (struct-copy result res [status status] [time runtime]))

(define (test-mutations file pname prob #:index [index (hash)])
  (eprintf "~a\t~a\t" file pname)
  (define prob* (dict-update prob ':documents (curry map dom-not-something)))
  (define res (make-result file pname prob #:index index))
  (define-values (out runtime) (run-problem prob*))
  (define status (get-status (list file pname) prob out #:invert true #:unsupported true))
  (eprintf "~a\n" status)
  (flush-output (current-error-port))
  (struct-copy result res [status status] [time runtime]))

(define (test-assertions assertion file pname prob #:index [index (hash)])
  (eprintf "~a\t~a\t~a\t" file pname assertion)
  (define prob* (dict-update prob ':documents (curry map (compose dom-set-range dom-strip-positions))))
  (define res (make-result file pname prob #:subproblem assertion #:index index))
  (define-values (out runtime) (run-problem prob* #:fuzz #f))
  (define status (get-status (list file pname assertion) prob out #:invert true #:unsupported false))

  (eprintf "~a\n" status)
  (flush-output (current-error-port))
  (struct-copy result res [status status] [time runtime]))

(define (termination-message all sent recv)
  (eprintf "\nTerminating after ~a/~a. Waiting for ~a\n"
           (length recv) (length all) (sort (set-subtract sent recv) <)))

(define-syntax-rule (for/threads num-threads ([input all-inputs]) body ...)
  (let* ([threads num-threads] [inputs all-inputs] [total (length inputs)])
    (cond
     [(not threads)
      (for/list ([input inputs] [n (in-naturals)])
        (with-handlers ([exn:break?
                         (λ (e)
                           (termination-message (range total) (range (+ n 1)) (range n))
                           (raise e))])
          body ...))]
     [else
      (define workers
        (for/list ([i (in-range threads)])
          (define-values (hd* vb* to* ef*)
            (values helper-dict (verbose) (timeout) (expected-failures)))
          (place/context ch
            (for ([(k v) (in-dict hd*)])
              (hash-set! helper-dict k v)
              (hash-set! assertion-helpers (car k)
                         (procedure-reduce-arity
                          (λ vals
                            (smt-replace-terms v (map cons (cdr k) vals)))
                          (length (cdr k)))))
            (verbose vb*)
            (timeout to*)
            (expected-failures ef*)
            
            ;; Main loop
            (let loop ()
              (match-define (list* self id thing) (place-channel-get ch))
              (with-handlers ([exn:fail?
                               (λ (e)
                                 ((error-display-handler) (exn-message e) e)
                                 (place-channel-put ch (list* self id)))])
                (define result (let ([input thing]) body ...))
                (place-channel-put ch (list* self id result)))
              (loop)))))
      (define to-send (map cons (range 0 (length inputs)) inputs))
      (for ([worker workers])
        (unless (null? to-send)
          (place-channel-put worker (cons worker (car to-send)))
          (set! to-send (cdr to-send))))
      (let loop ([out '()])
        (define sent (set-subtract (range total) (map car to-send)))
        (cond
         [(= (length out) (length inputs))
          (map cdr (sort out < #:key car))]
         [else
          (match-define (cons worker result) 
                        (with-handlers ([exn:break?
                                         (λ (e)
                                           (termination-message (range total) sent (map car out))
                                           (raise e))])
                          (apply sync workers)))
          (unless (pair? result)
            (termination-message (range total) sent (map car out))
            (exit 1))
          (unless (null? to-send)
            (place-channel-put worker (cons worker (car to-send)))
            (set! to-send (cdr to-send)))
          (loop (cons result out))]))])))

(define (run-regression-tests probs #:valid [valid? (const true)] #:index [index (hash)]
                              #:threads [threads #f])
  (define inputs
    (for/list ([(file x) (in-dict probs)] #:when (valid? (cdr x)))
      (list file (car x) (cdr x) index)))

  (for/threads threads ([rec inputs])
    (match-define (list file pname prob index) rec)
    (test-regression file pname prob #:index index)))

(define (run-mutation-tests probs #:repeat [repeat 1] #:valid [valid? (const true)] #:index [index (hash)]
                            #:threads [threads #f])
  (define inputs
    (for/list ([(file x) (in-dict probs)] #:when (valid? (cdr x))
               [_ (in-range repeat)])
      (list file (car x) (cdr x) index)))
  (for/threads threads ([rec inputs])
    (match-define (list file pname prob index) rec)
    (test-mutations file pname prob #:index index)))

(define (run-assertion-tests probs #:valid [valid? (const true)] #:index [index (hash)]
                             #:threads [threads #f])
  (define inputs
    (for/list ([(assertion x) (in-dict probs)] #:when (valid? (cddr x)))
      (list assertion (first x) (second x) (cddr x) index)))
  (for/threads threads ([rec inputs])
    (match-define (list assertion file pname prob index) rec)
    (test-assertions assertion file pname prob #:index index)))

(define (run-proofs-tests probs #:valid [valid? (const true)] #:index [index (hash)]
                          #:threads [threads #f])
  (define inputs
    (for/append ([(file x) (in-dict probs)] [n (in-naturals)] #:when (valid? (cdr x)))
      (append
       (for/list ([part (cddr x)] [i (in-naturals)])
         (define name (first (dict-ref part ':name (list i))))
         (list file name (car x) (cadr x) part index)))))

  (for/threads threads ([rec inputs])
    (match-define (list file name pname pname2 prob index) rec)
    (eprintf "~a\t~a\t~a\t~a~a" file pname pname2 name (if (verbose) "\n" "\t"))
    (define res (make-result (~a pname2) pname prob #:subproblem name #:index index))
    (define-values (out runtime) (run-problem prob))
    (define status (get-status (list file pname) prob out #:invert true #:unsupported true))
    (eprintf "~a\n" status)
    (flush-output (current-error-port))
    (struct-copy result res [status status] [time runtime])))


(define (file-name-stem fn)
  (define-values (_1 uname _2) (split-path fn))
  uname)

(define (call-with-output-to outname #:extension [extension #f] #:exists [exists 'error] f . args)
  (if outname
      (call-with-output-file (if extension (format "~a.~a" outname extension) outname) #:exists exists
        (apply curry f args))
      (apply f (append args (list (current-output-port))))))

(define (row #:cell [cell 'td] #:hide [hide #f] #:class [class #f] . args)
  `(tr (,@(if class `((class ,class)) '()))
       ,@(for/list ([arg args]) `(,cell () ,(if (equal? arg hide) "" arg)))))

(define (load-results file)
  (define data (call-with-input-file file read-json))
  (values
   (for/list ([rec (dict-ref data 'problems)])
     (define (get field [convert identity]) (convert (dict-ref rec field)))
     (result (get 'file) (get 'problem string->symbol) (and (get 'subproblem) (get 'subproblem string->symbol))
             (get 'test string->symbol) (get 'section)
             (match (get 'status string->symbol)
               [(or 'fail 'unsupported 'expected)
                (cond
                 [(apply expected? (get 'file) (get 'problem string->symbol)
                         (if (get 'subproblem)
                             (list (get 'subproblem string->symbol))
                             (list)))
                  'expected]
                 [(not (subset? (get 'features (curry map string->symbol)) (supported-features)))
                  'unsupported]
                 [else 'fail])]
               [s s])
             (get 'description) (get 'features (curry map string->symbol)) (get 'time) (get 'url)))
   (dict-ref data 'minimized #f)))

(define (shorten-filename name)
  (string-join (drop-right (string-split (~a (file-name-from-path name)) ".") 1) "."))

(define (write-json* results #:output [outname #f])
  (call-with-output-to
   outname #:extension "json" #:exists 'replace
   write-json
   (make-hash
    `((branch . ,*branch*)
      (commit . ,*commit*)
      (version . ,*version*)
      (problems
       . ,(for/list ([res results])
            (match-define (result file problem subproblem test section status description features time url) res)
            (make-hash
             `((file . ,(~a file))
               (problem . ,(~a problem))
               (subproblem . ,(and subproblem (~a subproblem)))
               (test . ,(~a test))
               (section . ,section)
               (status . ,(~a status))
               (description . ,description)
               (features . ,(map ~a features))
               (time . ,time)
               (url . ,url)))))))))

(define (status-symbol status)
  (match status
    ['success "✔"] ['fail "✘"] ['timeout "🕡"]
    ['unsupported "☹"] ['error "!"] ['expected "-"]
    ['ready "0"]))

(define (print-time ms)
  (cond
   [(< ms 2) (format "~ams" (~r ms #:precision 3))]
   [(< ms 2000) (format "~ams" (~r ms #:precision 1))]
   [(< ms 120000) (format "~as" (~r (/ ms 1000) #:precision 1))]
   [(< ms 7200000) (format "~amin" (~r (/ ms 60000) #:precision 1))]
   [else (format "~ahr" (~r (/ ms 3600000) #:precision 1))]))

(define (write-report results #:output [outname #f])
  (write-json* results #:output outname)
  (write-report* results #f #:output outname))

(define (write-report* results minimizer #:output [outname #f])
  (define total-time
    (apply + (map result-time results)))

  (define (count-type set t)
    (count (λ (x) (equal? (result-status x) t)) set))
  (define (set->results set)
    (map (compose number->string (curry count-type set)) '(success fail error timeout unsupported)))

  (define unsupported-features
    (set-subtract (remove-duplicates (append-map result-features results)) (supported-features)))

  (define (feature-row feature results)
    (list feature
          (count (λ (x) (equal? 
                         (set-subtract
                          (result-features x)
                          (if (set-member? (supported-features) feature)
                              (list)
                              (supported-features)))
                         (list feature))) results)
          (count (λ (x) (set-member? (result-features x) feature)) results)))

  (define (sort-features data)
    (filter (λ (r) (> (third r) 0)) (sort (sort data > #:key third) > #:key second)))

  (define (show-res res)
    (not (set-member?
          (if (show-success) '() '(success unsupported expected timeout))
          (result-status res))))

  (call-with-output-to
   outname #:extension "html" #:exists 'replace
   write-xexpr
   `(html ((lang "en_US"))
     (meta ((charset "utf8")))
     (link ((rel "stylesheet") (href "report.css")))
     (title ,(format "Cassius results for ~a" (string-join (remove-duplicates (map result-file results)) ", ")))
     (body
      (p (b "Cassius") " version " (kbd ,(~a *version*)) " branch " (kbd ,(~a *branch*)) " commit " (kbd ,(~a *commit*)))
      (p (b "Time") " total " ,(print-time total-time) " for " ,(~a (length results)) " tests.")
      (table ((id "sections") (rules "groups") (class "numbers"))
       (thead
        ,(row #:cell 'th "" "Pass" "Fail" "Error" "Time" "Skip" "")
        ,(apply row `(strong "Total") (append (set->results results) '(""))))
       (tbody
        ,@(for/list ([section (sort (remove-duplicates (map result-section results)) section<?)])
            (define sresults (filter (λ (x) (equal? (result-section x) section)) results))
            (keyword-apply
             row '(#:hide) '("0")
             (string-replace section "s" "§" #:all? #f)
             (append
              (set->results sresults)
              `((span
                 ,@(for/list ([r sresults] #:when (member (result-status r) '(error fail)))
                     `(a ((href ,(result-url r)))
                         ,(format "~a:~a" (file-name-stem (result-file r)) (result-problem r)))))))))))
      ,(if (ormap (λ (r) (set-member? '(unsupported) (result-status r))) results)
           `(section
              (h2 "Feature totals")
              (table ([class "numbers"])
               (thead ,(row #:cell 'th "Unsupported Feature" "# Blocking" "# Necessary"))
               (tbody
                      ,@(let ([bad-results
                               (for/list ([r results] #:when (not (set-member? '(success expected) (result-status r))))
                                 r)])
                          (for/list ([data (sort-features (map (curryr feature-row bad-results) unsupported-features))])
                            (apply row (map ~a data)))))))
           "")
      ,(if minimizer
           `(section
             (h2 "Minimizer results")
             (table ([class "numbers"])
              (thead ,(row #:cell 'th "Problem" "Iterations" "Before" "After" "Time"))
              ,@(for/list ([(name rec) minimizer])
                  (row `(a ([href ,(dict-ref rec 'path)]) ,(~a name))
                       (~a (dict-ref rec 'iterations))
                       (~a (dict-ref rec 'initial))
                       (~a (dict-ref rec 'final))
                       (print-time (dict-ref rec 'time))))))
           "")
      (section
       (h2 ,(if (show-success) "Tests" "Failing tests"))
       (table
       ,@(for/list ([results-group (group-by result-file results)]
                    #:unless (not (ormap show-res results-group)))
           `(tbody
             (tr (th ((colspan "4")) ,(result-file (car results-group))))
             ,@(for/list ([ress (group-by result-problem results-group)]
                          #:unless (not (ormap show-res ress)))
                 (match-define (result file problem _ test section _ description features _ url) (car ress))
                 (row
                  `(div
                    ,@(for/list ([res ress])
                        `(span ([class ,(~a (result-status res))]
                                [title ,(format "~a\nTime: ~a" (or (result-subproblem res) "") (print-time (result-time res)))])
                               ,(status-symbol (result-status res)))))
                  (~a problem) `(a ([href ,url]) ,(~a test)) description))))))))))

(define (print-feature-table problems)
  (define all-features (remove-duplicates (append-map (λ (x) (dict-ref x ':features '())) problems)))
  (define unsupported-features (set-subtract all-features (supported-features)))

  (define width (apply max (map (compose string-length ~a) (cons "Feature" all-features))))
  (define (~feature feature) (~a feature #:width width))

  (define (feature-row feature)
    (list feature
          (count (λ (x) (equal? 
                         (set-subtract
                          (dict-ref x ':features '())
                          (if (set-member? (supported-features) feature)
                              (list)
                              (supported-features)))
                         (list feature))) problems)
          (count (λ (x) (member feature (dict-ref x ':features '()))) problems)))

  (define (sort-features data)
    (sort (sort data > #:key third) > #:key second))

  (printf "~a\t~a\t~a\n" (~feature "Feature") "#B" "#N")
  (for ([data (sort-features (map feature-row unsupported-features))])
    (printf "~a\t~a\t~a\n" (~feature (first data)) (second data) (third data)))

  (printf "\n~a\t~a\t~a\n" (~feature "Feature") "#B" "#N")
  (for ([data (sort-features (map feature-row (supported-features)))])
    (printf "~a\t~a\t~a\n" (~feature (first data)) (second data) (third data)))

  (printf "\n~a unsupported tests\n"
          (count (λ (prob) (not (subset? (dict-ref prob ':features '()) (supported-features)))) problems)))

(define-syntax-rule (and! var function)
  (set! var (let ([fn function] [test var]) (λ (x) (and (fn x) (test x))))))

(define (read-index iname)
  (for*/hash ([sec (call-with-input-file iname read-json)]
              [(k v) (in-hash sec)])
    (define name
      (if (string=? (last (string-split (~a k) "-")) (substring v 1))
          (string-join (drop-right (string-split (~a k) "-") 1) "-")
          k))
    (values name v)))

(define (get-index index uname)
  (define base (first (string-split (~a uname) ".")))
  (hash-ref index
            (if (string=? (last (string-split base "-")) "ref")
                (string-join (drop-right (string-split base "-") 1) "-")
                base)
            "(unknown)"))

(define (read-failed-tests jname)
  (define failed-tests
    (for/list ([rec (hash-ref (call-with-input-file jname read-json) 'problems)]
               #:unless (equal? (dict-ref rec 'status) "success"))
      (dict-ref rec 'test)))

  (λ (p) (set-member? failed-tests (~a (file-name-stem (car (dict-ref p ':url '("/tmp"))))))))

(module+ main
  (define out-file #f)
  (define index (hash))
  (define valid? (const true))
  (define repeat 1)
  (define threads #f)

  (multi-command-line
   #:program "report"

   #:multi
   [("-d" "--debug") "Turn on debug mode" (debug-mode!)]
   [("--cache") file-name "Cache for Z3 results"
    (*cache-file* file-name)
    (when (file-exists? file-name)
      (call-with-input-file file-name
        (λ (p)
          (for ([(k v) (in-dict (read p))])
            (hash-set! *cache* k v)))))]

   #:once-each
   [("-o" "--output") fname "File name for final CSS file"
    (set! out-file fname)]
   [("-t" "--timeout") s "Timeout in seconds"
    (timeout (string->number s))]
   [("-v" "--verbose") "Print output of each solver process"
    (verbose true)]
   [("--index") index-file "File name with section information for tests"
    (set! index (read-index index-file))]
   [("--show-all") "Do not hide successful or unsupported tests"
    (show-success true)]
   [("--supported") "Skip tests with unsupported features"
    (and! valid? (λ (p) (subset? (dict-ref p ':features '()) (supported-features))))]
   [("--failed") json-file "Run only tests that failed in given JSON file"
    (and! valid? (read-failed-tests json-file))]
   [("--sections") sections "Run only tests for particular sections (needs --index)"
    (define secs (string-split sections ","))
    (define (valid-sections? prob)
      (define url (car (dict-ref prob ':url '("/tmp"))))
      (set-member? secs (get-index index (file-name-stem url))))
    (and! valid? valid-sections?)]
   [("--feature") feature "Test a particular feature"
    (and! valid? (λ (p) (set-member? (dict-ref p ':features '()) (string->symbol feature))))]
   [("--expected") efile "Expect failures named in this file"
    (expected-failures (call-with-input-file efile (λ (p) (sequence->list (in-port read p)))))]
   [("--threads") t "How many threads to use"
    (set! threads (string->number t))]

   #:subcommands

   ["regression"
    #:args fnames
    (write-report
     #:output out-file
     (let ([probs (for/append ([file (sort fnames string<?)])
                              (define x (sort (hash->list (call-with-input-file file parse-file)) symbol<? #:key car))
                              (map (curry cons file) x))])
       (run-regression-tests probs #:valid valid? #:index index #:threads threads)))]

   ["mutation"
    #:once-each
    [("-n" "--repeat") n "How many random bugs to try per test"
     (set! repeat (string->number n))]
    #:args fnames
    (write-report
     #:output out-file
     (let ([probs (for/append ([file (sort fnames string<?)])
                              (define x (sort (hash->list (call-with-input-file file parse-file)) symbol<? #:key car))
                              (map (curry cons file) x))])
       (run-mutation-tests probs #:valid valid? #:index index #:repeat repeat #:threads threads)))]

   ["features"
    #:args fnames
    (print-feature-table
     (for/append ([file fnames]) (dict-values (call-with-input-file file parse-file))))]

   ["available"
    #:args fnames
    (for* ([file fnames] [(name prob) (in-dict (call-with-input-file file parse-file))]
           #:when (subset? (dict-ref prob ':features '()) (supported-features)))
      (printf "~a ~a\n" file name))]

   ["assertions"
    #:args (assertions . fnames)
    (define prob1
      (for/append ([file (sort fnames string<?)])
                  (define x (sort (hash->list (call-with-input-file file parse-file)) symbol<? #:key car))
                  (map (curry cons file) x)))
    (define assertions*
      (call-with-input-file assertions
        (λ (p) (sequence->list (in-port read p)))))

    (define probs
      (for*/list ([prob prob1] [assertion assertions*])
        (match-define `(define-test (,name ,args ...) ,body) assertion)
        (match-define (cons a (cons b c)) prob)
        (list* name a b (dict-set c ':tests (list `(forall ,args ,body))))))
    (write-report
     #:output out-file
     (run-assertion-tests probs #:valid valid? #:index index #:threads threads))]

   ["specific-assertions"
    #:args (assertions file problems)
    (define assns
      (call-with-input-file assertions
        (λ (p) (for/hash ([ass (sequence->list (in-port read p))])
                 (match-define `(define-test (,name ,args ...) ,body) ass)
                 (values name `(forall ,args ,body))))))
    (define probs (call-with-input-file file parse-file))

    (define insts
      (call-with-input-file problems
        (λ (f)
          (for/list ([x (in-port read f)])
            (list* (second x) file (first x) (dict-set (dict-ref probs (first x)) ':tests (list (dict-ref assns (second x)))))))))

    (write-report
     #:output out-file
     (run-assertion-tests insts #:valid valid? #:index index #:threads threads))]

   ["proofs"
    #:args fnames
    (write-report
     #:output out-file
     (let ([probs (for/append ([file (sort fnames string<?)])
                              (define x (sort
                                         (append-map
                                          (λ (x) (map (curry cons (car x)) (dict->list (cdr x))))
                                          (dict->list
                                           (call-with-input-file file
                                             (λ (p) 
                                               (parameterize ([current-directory (path-tail file)])
                                                 (read-proofs p))))))
                                          symbol<? #:key car))
                              (map (curry cons file) x))])
       (run-proofs-tests probs #:valid valid? #:index index #:threads threads)))]

   ["rerender"
    #:args (json-file)
    (define-values (results minimizer) (load-results json-file))
    (write-report* #:output out-file results minimizer)]))