tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 8 forks source link

do-time #210

Closed bennn closed 1 year ago

bennn commented 1 year ago

add a macro to time things

looks like startup takes 1 second before anything can happen in Forge land

my output for an empty forge/core file:

$  PLTSTDERR="error debug@forge-timing" bracket core-empty.rkt
forge-timing: Starting                                 at 1137
forge-timing: forge/lang/reader                        at 1137  last step: 0    gc: 0   total: 0
forge-timing: forge-core-mod toplevel                  at 1549  last step: 412  gc: 182 total: 412
forge-timing: forge-core-mod require                   at 1549  last step: 0    gc: 0   total: 412
forge-timing: forge-core-mod parse-tree                at 1549  last step: 0    gc: 0   total: 412
bennn commented 1 year ago

We can add (begin-for-syntax (require forge/shared) (do-time "for-syntax WHATEVER")) at the top of a file, and that'll report a time during macro expansion.

But, if I compile the program first (raco make), then macros don't expand when I run racket , and there's still a 1-sec startup cost.

ALSO the logs print several times when compiling and need extra racket/base requires at for-syntax so I will not add them here

bennn commented 1 year ago

Other news: logger code has no cost if nobody is subscribed to the logger.

Example:

#lang racket/base

(define-logger foo)

(define (f)
  (for/fold ((acc '()))
            ((n (in-range 20000)))
    (cons n (reverse acc))))

;; (void (f))
;; 3 seconds

(log-foo-debug "wow ~s" (car (f)))
;; 0.2 seconds if nobody listening to the foo logger
;;  time racket file.rkt
;;  or even: time PLTSTDERR="error info@foo" racket file.rkt
;; 3 seconds if listeners
;;  time PLTSTDERR="error debug@foo" racket file.rkt