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 Total time 5980 ms Parsing 4 ms Import 0 ms Deserialization 0 ms Scoping 56 ms Typing 212 ms Termination 0 ms Positivity 0 ms Injectivity 0 ms ProjectionLikeness 0 ms Coverage 0 ms Highlighting 0 ms Serialization 536 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,762,844,552 bytes allocated in the heap 760,074,864 bytes copied during GC 18,477,560 bytes maximum residency (41 sample(s)) 950,720 bytes maximum slop 54 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5235 colls, 0 par 1.48s 1.49s 0.0003s 0.0071s Gen 1 41 colls, 0 par 1.02s 1.02s 0.0249s 0.0545s INIT time 0.00s ( 0.00s elapsed) MUT time 3.49s ( 3.63s elapsed) GC time 2.49s ( 2.51s elapsed) EXIT time 0.01s ( 0.01s elapsed) Total time 5.99s ( 6.15s elapsed) %GC time 41.6% (40.9% elapsed) Alloc rate 791,916,986 bytes per MUT second Productivity 58.4% of total user, 56.9% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 3028544 972492 16872 Swap: 13309816 784388 12525428 Bootup: Fri Mar 21 07:39:33 2014 Load average: 2.75 1.55 0.89 4/539 27862 user : 03:04:02.23 12.3% page in : 7285739 nice : 00:02:38.47 0.2% page out: 13893300 system: 00:45:29.48 3.0% page act: 3079637 IOwait: 00:24:10.42 1.6% page dea: 1689774 hw irq: 00:00:02.78 0.0% page flt: 64627250 sw irq: 00:01:57.68 0.1% swap in : 99438 idle : 20:37:11.47 82.7% swap out: 241354 uptime: 2d 03:33:50.50 context : 91469731 irq 0: 10143519 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 161743 i8042 irq 21: 353767 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 738 ehci_hcd:usb1, uh irq 9: 25668 acpi irq 43: 789192 ahci irq 12: 101297 i8042 irq 44: 62065 eth0 irq 17: 1312 firewire_ohci irq 45: 6640645 i915 irq 18: 0 mmc0 irq 46: 8181891 iwlwifi irq 19: 0 yenta irq 47: 144 snd_hda_intel sda 546383r 205196w eth0 TX 30.30MiB RX 332.57MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 360.50KiB RX 360.50KiB