123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293 |
- Ticks for Basics
- max-open-constraints = 0
- max-open-metas = 1
- metas = 13
- Ticks for Pr
- max-open-constraints = 0
- max-open-metas = 3
- metas = 88
- Ticks for Nom
- max-open-constraints = 2
- max-open-metas = 4
- attempted-constraints = 8
- metas = 87
- Ticks for Kind
- max-open-constraints = 0
- max-open-metas = 1
- metas = 10
- Ticks for Cxt
- max-open-constraints = 0
- max-open-metas = 1
- metas = 59
- Ticks for Loc
- max-open-constraints = 0
- max-open-metas = 6
- metas = 145
- Ticks for Term
- max-open-constraints = 2
- attempted-constraints = 4
- max-open-metas = 10
- metas = 241
- Ticks for Shift
- max-open-constraints = 2
- max-open-metas = 14
- attempted-constraints = 16
- metas = 230
- Ticks for Eta
- max-open-constraints = 2
- attempted-constraints = 12
- max-open-metas = 18
- metas = 185
- Ticks for Inst
- max-open-constraints = 2
- attempted-constraints = 9
- max-open-metas = 16
- metas = 276
- Ticks for Subst
- max-open-constraints = 2
- attempted-constraints = 8
- max-open-metas = 13
- metas = 202
- Ticks for Syntacticosmos
- max-open-constraints = 0
- max-open-metas = 1
- metas = 1
- Ticks for UntypedLambda
- max-open-constraints = 2
- attempted-constraints = 20
- max-open-metas = 23
- metas = 101
- agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
- 1,715,843,520 bytes allocated in the heap
- 377,143,448 bytes copied during GC
- 11,317,764 bytes maximum residency (37 sample(s))
- 215,024 bytes maximum slop
- 30 MB total memory in use (0 MB lost due to fragmentation)
- Generation 0: 3214 collections, 0 parallel, 0.98s, 1.00s elapsed
- Generation 1: 37 collections, 0 parallel, 0.66s, 0.71s elapsed
- INIT time 0.00s ( 0.00s elapsed)
- MUT time 3.88s ( 3.95s elapsed)
- GC time 1.64s ( 1.70s elapsed)
- EXIT time 0.00s ( 0.00s elapsed)
- Total time 5.52s ( 5.65s elapsed)
- %GC time 29.7% (30.1% elapsed)
- Alloc rate 442,611,574 bytes per MUT second
- Productivity 70.3% of total user, 68.6% of total elapsed
- ──────────────────────────────────────────────────────────────────
- Mach kernel version:
- Darwin Kernel Version 9.8.0: Wed Jul 15 16:55:01 PDT 2009; root:xnu-1228.15.4~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: 59 tasks, 197 threads, 2 processors
- Load average: 1.00, Mach factor: 0.99
|