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 2,750,639,864 bytes allocated in the heap 739,125,192 bytes copied during GC 16,760,264 bytes maximum residency (42 sample(s)) 914,368 bytes maximum slop 47 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5213 colls, 0 par 1.21s 1.21s 0.0002s 0.0014s Gen 1 42 colls, 0 par 0.84s 0.84s 0.0201s 0.0411s INIT time 0.00s ( 0.00s elapsed) MUT time 2.91s ( 3.03s elapsed) GC time 2.06s ( 2.06s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 4.97s ( 5.09s elapsed) %GC time 41.4% (40.4% elapsed) Alloc rate 946,092,779 bytes per MUT second Productivity 58.6% of total user, 57.2% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 3717332 283704 128140 Swap: 13309816 66584 13243232 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.47 0.25 0.21 1/474 18859 user : 00:55:18.76 7.0% page in : 2921947 nice : 00:02:12.12 0.3% page out: 2894764 system: 00:18:35.44 2.4% page act: 592535 IOwait: 00:11:08.79 1.4% page dea: 260545 hw irq: 00:00:01.36 0.0% page flt: 18488748 sw irq: 00:00:49.57 0.1% swap in : 8 idle : 11:40:24.75 88.8% swap out: 16717 uptime: 1d 04:57:17.03 context : 35650173 irq 0: 2479016 timer irq 20: 8 ehci_hcd:usb2, uh irq 1: 59176 i8042 irq 21: 203713 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 460 ehci_hcd:usb1, uh irq 9: 11923 acpi irq 43: 355712 ahci irq 12: 54989 i8042 irq 44: 100161 eth0 irq 17: 622 firewire_ohci irq 45: 3850587 i915 irq 18: 0 mmc0 irq 46: 3444402 iwlwifi irq 19: 0 yenta irq 47: 145 snd_hda_intel sda 242723r 88134w eth0 TX 9.83MiB RX 134.22MiB wlan0 TX 13.06MiB RX 56.69MiB lo TX 269.66KiB RX 269.66KiB