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 5060 ms Parsing 4 ms Import 4 ms Deserialization 0 ms Scoping 44 ms Typing 188 ms Termination 0 ms Positivity 0 ms Injectivity 0 ms ProjectionLikeness 0 ms Coverage 0 ms Highlighting 4 ms Serialization 448 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,762,960,856 bytes allocated in the heap 762,762,640 bytes copied during GC 18,550,936 bytes maximum residency (41 sample(s)) 933,560 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.24s 1.24s 0.0002s 0.0014s Gen 1 41 colls, 0 par 0.89s 0.89s 0.0218s 0.0447s INIT time 0.00s ( 0.00s elapsed) MUT time 2.92s ( 2.99s elapsed) GC time 2.13s ( 2.14s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 5.06s ( 5.14s elapsed) %GC time 42.2% (41.6% elapsed) Alloc rate 945,283,684 bytes per MUT second Productivity 57.8% of total user, 57.0% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2694592 1306444 8120 Swap: 13309816 748128 12561688 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.48 0.32 0.35 1/498 22881 user : 02:45:22.26 11.0% page in : 5714579 nice : 00:02:17.68 0.2% page out: 12731764 system: 00:40:56.44 2.7% page act: 2697371 IOwait: 00:20:33.64 1.4% page dea: 1347335 hw irq: 00:00:02.54 0.0% page flt: 59456421 sw irq: 00:01:49.39 0.1% swap in : 94151 idle : 21:10:37.91 84.6% swap out: 224353 uptime: 1d 15:33:01.81 context : 83662159 irq 0: 8682305 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 159859 i8042 irq 21: 344134 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 670 ehci_hcd:usb1, uh irq 9: 25306 acpi irq 43: 648384 ahci irq 12: 101141 i8042 irq 44: 79859 eth0 irq 17: 1194 firewire_ohci irq 45: 6383814 i915 irq 18: 0 mmc0 irq 46: 7718890 iwlwifi irq 19: 0 yenta irq 47: 153 snd_hda_intel sda 425968r 187268w eth0 TX 24.38MiB RX 257.07MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 326.70KiB RX 326.70KiB