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 5132 ms Parsing 68 ms Import 0 ms Deserialization 0 ms Scoping 360 ms Typing 6088 ms Termination 184 ms Positivity 292 ms Injectivity 4 ms ProjectionLikeness 0 ms Coverage 128 ms Highlighting 104 ms Serialization 3064 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,765,142,176 bytes allocated in the heap 765,387,808 bytes copied during GC 18,079,952 bytes maximum residency (42 sample(s)) 948,048 bytes maximum slop 49 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5239 colls, 0 par 1.26s 1.26s 0.0002s 0.0030s Gen 1 42 colls, 0 par 0.91s 0.91s 0.0218s 0.0471s INIT time 0.00s ( 0.00s elapsed) MUT time 2.97s ( 3.03s elapsed) GC time 2.17s ( 2.17s elapsed) EXIT time 0.01s ( 0.01s elapsed) Total time 5.14s ( 5.21s elapsed) %GC time 42.2% (41.8% elapsed) Alloc rate 932,553,128 bytes per MUT second Productivity 57.8% of total user, 57.1% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2623336 1377700 16860 Swap: 13309816 849524 12460292 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.20 0.34 0.57 1/497 15595 user : 05:11:13.16 14.3% page in : 9647727 nice : 00:02:38.50 0.1% page out: 20025288 system: 01:02:14.46 2.9% page act: 4552838 IOwait: 00:31:26.09 1.4% page dea: 2366056 hw irq: 00:00:03.36 0.0% page flt: 160031806 sw irq: 00:02:23.34 0.1% swap in : 110175 idle : 1d 05:23:13.74 81.1% swap out: 276865 uptime: 2d 09:16:07.86 context : 118267728 irq 0: 14189599 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 190729 i8042 irq 21: 480322 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 738 ehci_hcd:usb1, uh irq 9: 25668 acpi irq 43: 999694 ahci irq 12: 101618 i8042 irq 44: 204736 eth0 irq 17: 1632 firewire_ohci irq 45: 8087126 i915 irq 18: 0 mmc0 irq 46: 9542929 iwlwifi irq 19: 0 yenta irq 47: 144 snd_hda_intel sda 654686r 301443w eth0 TX 41.26MiB RX 412.29MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 388.86KiB RX 388.86KiB