123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151 |
- Ticks for Agda.Primitive
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 1
- metas = 5
- equal terms = 9
- Ticks for Basics
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 1
- unequal terms = 2
- metas = 13
- equal terms = 23
- Ticks for Pr
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 3
- unequal terms = 17
- metas = 88
- equal terms = 172
- Ticks for Nom
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- max-open-metas = 4
- attempted-constraints = 8
- unequal terms = 77
- metas = 79
- equal terms = 207
- Ticks for Kind
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 1
- metas = 10
- equal terms = 20
- Ticks for Cxt
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 1
- unequal terms = 7
- metas = 30
- equal terms = 157
- Ticks for Loc
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 6
- metas = 130
- unequal terms = 145
- equal terms = 320
- Ticks for Term
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 4
- max-open-metas = 10
- unequal terms = 140
- metas = 243
- equal terms = 598
- Ticks for Shift
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- max-open-metas = 14
- attempted-constraints = 16
- metas = 225
- unequal terms = 396
- equal terms = 639
- Ticks for Eta
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 12
- max-open-metas = 18
- metas = 177
- unequal terms = 263
- equal terms = 467
- Ticks for Inst
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 9
- max-open-metas = 16
- metas = 263
- unequal terms = 538
- equal terms = 878
- Ticks for Subst
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 8
- max-open-metas = 13
- metas = 189
- unequal terms = 314
- equal terms = 537
- Ticks for Syntacticosmos
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 1
- metas = 1
- equal terms = 21
- Ticks for UntypedLambda
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 20
- max-open-metas = 23
- metas = 101
- unequal terms = 124
- equal terms = 180
- agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
- 4,425,378,728 bytes allocated in the heap
- 915,294,472 bytes copied during GC
- 42,370,080 bytes maximum residency (44 sample(s))
- 895,816 bytes maximum slop
- 100 MB total memory in use (0 MB lost due to fragmentation)
- Tot time (elapsed) Avg pause Max pause
- Gen 0 8445 colls, 0 par 1.07s 1.08s 0.0001s 0.0011s
- Gen 1 44 colls, 0 par 0.73s 0.78s 0.0177s 0.0720s
- INIT time 0.00s ( 0.00s elapsed)
- MUT time 3.31s ( 3.38s elapsed)
- GC time 1.80s ( 1.86s elapsed)
- EXIT time 0.00s ( 0.00s elapsed)
- Total time 5.12s ( 5.25s elapsed)
- %GC time 35.2% (35.5% elapsed)
- Alloc rate 1,335,573,905 bytes per MUT second
- Productivity 64.8% of total user, 63.2% of total elapsed
- ──────────────────────────────────────────────────────────────────
- Mach kernel version:
- Darwin Kernel Version 13.0.0: Thu Sep 19 22:22:27 PDT 2013; root:xnu-2422.1.72~6/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: 16.00 gigabytes
- Default processor set: 327 tasks, 1536 threads, 8 processors
- Load average: 3.26, Mach factor: 4.73
|