123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144 |
- 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 = 75
- metas = 87
- equal terms = 216
- 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 = 5
- metas = 59
- equal terms = 190
- Ticks for Loc
- max-open-constraints = 0
- pointers = 0
- pointers (reused) = 0
- max-open-metas = 6
- metas = 145
- unequal terms = 145
- equal terms = 335
- Ticks for Term
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 4
- max-open-metas = 10
- unequal terms = 158
- metas = 241
- equal terms = 615
- Ticks for Shift
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- max-open-metas = 14
- attempted-constraints = 16
- metas = 230
- unequal terms = 412
- equal terms = 639
- Ticks for Eta
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 12
- max-open-metas = 18
- metas = 185
- unequal terms = 270
- equal terms = 487
- Ticks for Inst
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 9
- max-open-metas = 16
- metas = 276
- unequal terms = 534
- equal terms = 948
- Ticks for Subst
- pointers = 0
- pointers (reused) = 0
- max-open-constraints = 2
- attempted-constraints = 8
- max-open-metas = 13
- metas = 202
- unequal terms = 315
- equal terms = 576
- 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 (null)
- 1,729,921,352 bytes allocated in the heap
- 330,880,688 bytes copied during GC
- 13,587,564 bytes maximum residency (33 sample(s))
- 238,368 bytes maximum slop
- 34 MB total memory in use (0 MB lost due to fragmentation)
- Tot time (elapsed) Avg pause Max pause
- Gen 0 3273 colls, 0 par 0.94s 1.00s 0.0003s 0.0200s
- Gen 1 33 colls, 0 par 0.64s 0.71s 0.0216s 0.0660s
- INIT time 0.00s ( 0.00s elapsed)
- MUT time 3.87s ( 4.05s elapsed)
- GC time 1.59s ( 1.72s elapsed)
- EXIT time 0.00s ( 0.00s elapsed)
- Total time 5.46s ( 5.77s elapsed)
- %GC time 29.1% (29.7% elapsed)
- Alloc rate 446,915,138 bytes per MUT second
- Productivity 70.9% of total user, 67.1% of total elapsed
- ──────────────────────────────────────────────────────────────────
- Mach kernel version:
- Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
- Kernel configured for up to 2 processors.
- 2 processors are physically available.
- 2 processors are logically available.
- Processor type: i486 (Intel 80486)
- Processors active: 0 1
- Primary memory available: 2.00 gigabytes
- Default processor set: 112 tasks, 504 threads, 2 processors
- Load average: 1.14, Mach factor: 0.88
|