Ticks for Basics max-open-constraints = 0 max-open-metas = 5 metas = 27 Ticks for Pr max-open-constraints = 0 max-open-metas = 4 metas = 168 Ticks for Nom max-open-constraints = 2 max-open-metas = 6 attempted-constraints = 8 metas = 132 Ticks for Kind max-open-constraints = 0 max-open-metas = 4 metas = 21 Ticks for Cxt max-open-constraints = 0 max-open-metas = 4 metas = 82 Ticks for Loc max-open-constraints = 0 max-open-metas = 6 metas = 178 Ticks for Term max-open-constraints = 2 attempted-constraints = 4 max-open-metas = 10 metas = 312 Ticks for Shift max-open-constraints = 2 max-open-metas = 14 attempted-constraints = 16 metas = 265 Ticks for Eta max-open-constraints = 2 attempted-constraints = 12 max-open-metas = 18 metas = 217 Ticks for Inst max-open-constraints = 2 attempted-constraints = 9 max-open-metas = 16 metas = 317 Ticks for Subst max-open-constraints = 2 attempted-constraints = 8 max-open-metas = 13 metas = 242 Ticks for Syntacticosmos max-open-constraints = 0 max-open-metas = 2 metas = 5 Ticks for UntypedLambda max-open-constraints = 2 attempted-constraints = 20 max-open-metas = 23 metas = 110 agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,225,271,480 bytes allocated in the heap 397,496,452 bytes copied during GC 11,303,508 bytes maximum residency (38 sample(s)) 244,604 bytes maximum slop 33 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 4201 colls, 0 par 0.77s 0.78s 0.0002s 0.0012s Gen 1 38 colls, 0 par 0.50s 0.51s 0.0134s 0.0343s INIT time 0.00s ( 0.00s elapsed) MUT time 3.21s ( 3.42s elapsed) GC time 1.27s ( 1.29s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 4.49s ( 4.71s elapsed) %GC time 28.3% (27.4% elapsed) Alloc rate 691,480,962 bytes per MUT second Productivity 71.7% of total user, 68.3% of total elapsed ────────────────────────────────────────────────────────────────── Mach kernel version: Darwin Kernel Version 11.3.0: Thu Jan 12 18:47:41 PST 2012; root:xnu-1699.24.23~1/RELEASE_X86_64 Kernel configured for up to 8 processors. 4 processors are physically available. 8 processors are logically available. Processor type: i486 (Intel 80486) Processors active: 0 1 2 3 4 5 6 7 Primary memory available: 8.00 gigabytes Default processor set: 109 tasks, 508 threads, 8 processors Load average: 1.42, Mach factor: 6.56