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 5072 ms Parsing 4 ms Import 0 ms Deserialization 0 ms Scoping 4564 ms Typing 200 ms Termination 0 ms Positivity 0 ms Injectivity 0 ms ProjectionLikeness 0 ms Highlighting 0 ms Serialization 444 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,762,041,264 bytes allocated in the heap 774,218,904 bytes copied during GC 19,561,392 bytes maximum residency (42 sample(s)) 926,056 bytes maximum slop 53 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5233 colls, 0 par 1.25s 1.26s 0.0002s 0.0039s Gen 1 42 colls, 0 par 0.92s 0.92s 0.0220s 0.0489s INIT time 0.00s ( 0.00s elapsed) MUT time 2.90s ( 3.20s elapsed) GC time 2.17s ( 2.18s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 5.08s ( 5.38s elapsed) %GC time 42.7% (40.5% elapsed) Alloc rate 951,776,091 bytes per MUT second Productivity 57.2% of total user, 54.0% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2696820 1304216 11296 Swap: 13309816 700548 12609268 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.58 0.32 0.27 1/473 15129 user : 02:21:11.42 10.9% page in : 5135375 nice : 00:02:17.56 0.2% page out: 10383848 system: 00:37:01.17 2.8% page act: 2123440 IOwait: 00:18:21.27 1.4% page dea: 1094268 hw irq: 00:00:02.33 0.0% page flt: 48642730 sw irq: 00:01:43.23 0.1% swap in : 92170 idle : 18:18:36.94 84.6% swap out: 211122 uptime: 1d 13:50:56.69 context : 76756331 irq 0: 7571097 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 148470 i8042 irq 21: 319982 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 665 ehci_hcd:usb1, uh irq 9: 21946 acpi irq 43: 603175 ahci irq 12: 101096 i8042 irq 44: 32076 eth0 irq 17: 1098 firewire_ohci irq 45: 5969812 i915 irq 18: 0 mmc0 irq 46: 7312239 iwlwifi irq 19: 0 yenta irq 47: 142 snd_hda_intel sda 403290r 166483w eth0 TX 21.17MiB RX 232.57MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 304.36KiB RX 304.36KiB