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 5056 ms Parsing 64 ms Import 8 ms Deserialization 0 ms Scoping 344 ms Typing 812 ms Termination 228 ms Positivity 304 ms Injectivity 4 ms ProjectionLikeness 0 ms Coverage 112 ms Highlighting 84 ms Serialization 3020 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,764,293,248 bytes allocated in the heap 755,940,248 bytes copied during GC 19,161,328 bytes maximum residency (41 sample(s)) 916,256 bytes maximum slop 53 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5238 colls, 0 par 1.24s 1.26s 0.0002s 0.0173s Gen 1 41 colls, 0 par 0.89s 0.90s 0.0219s 0.0462s INIT time 0.00s ( 0.00s elapsed) MUT time 2.93s ( 3.00s elapsed) GC time 2.13s ( 2.16s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 5.06s ( 5.17s elapsed) %GC time 42.1% (41.8% elapsed) Alloc rate 944,527,327 bytes per MUT second Productivity 57.9% of total user, 56.7% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2730428 1270608 49632 Swap: 13309816 1231704 12078112 Bootup: Fri Mar 21 07:39:35 2014 Load average: 0.66 0.95 1.08 1/521 23417 user : 06:45:35.68 17.3% page in : 11868467 nice : 00:02:42.68 0.1% page out: 22296072 system: 01:24:15.55 3.6% page act: 4973457 IOwait: 00:39:32.92 1.7% page dea: 2946590 hw irq: 00:00:04.33 0.0% page flt: 171632293 sw irq: 00:02:55.46 0.1% swap in : 258940 idle : 1d 06:03:34.83 77.1% swap out: 492243 uptime: 2d 15:32:39.81 context : 156051732 irq 0: 18586732 timer irq 20: 12 ehci_hcd:usb2, uh irq 1: 252873 i8042 irq 21: 545875 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 903600 ehci_hcd:usb1, uh irq 9: 36484 acpi irq 43: 1250114 ahci irq 12: 188270 i8042 irq 44: 540420 eth0 irq 17: 1919 firewire_ohci irq 45: 9511027 i915 irq 18: 0 mmc0 irq 46: 10552410 iwlwifi irq 19: 0 yenta irq 47: 911 snd_hda_intel sda 853364r 347285w eth0 TX 246.53MiB RX 494.39MiB wlan0 TX 24.08MiB RX 82.43MiB lo TX 580.42KiB RX 580.42KiB