Ticks for Agda.Primitive max-open-constraints = 0 pointers = 0 pointers (reused) = 0 max-open-metas = 1 metas = 5 equal terms = 9 Ticks for Data max-open-constraints = 0 pointers = 0 pointers (reused) = 0 max-open-metas = 14 equal terms = 153 metas = 160 unequal terms = 243 168 ms Parsing 4 ms Import 0 ms Deserialization 0 ms Scoping 12 ms Typing 388 ms Termination 0 ms Positivity 4 ms Injectivity 0 ms ProjectionLikeness 0 ms Highlighting 0 ms Serialization 44 ms agda -v0 -v profile:100 proj/Data.agda -iproj --ignore-interfaces +RTS -slogs/.tmp 107,599,680 bytes allocated in the heap 24,341,880 bytes copied during GC 3,643,336 bytes maximum residency (7 sample(s)) 206,256 bytes maximum slop 10 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 199 colls, 0 par 0.04s 0.04s 0.0002s 0.0005s Gen 1 7 colls, 0 par 0.04s 0.04s 0.0059s 0.0110s INIT time 0.00s ( 0.00s elapsed) MUT time 0.09s ( 0.10s elapsed) GC time 0.08s ( 0.08s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 0.17s ( 0.18s elapsed) %GC time 45.6% (43.1% elapsed) Alloc rate 1,185,394,538 bytes per MUT second Productivity 54.3% of total user, 51.2% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2701152 1299884 11660 Swap: 13309816 700548 12609268 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.70 0.36 0.28 1/472 15231 user : 02:21:29.88 10.9% page in : 5140123 nice : 00:02:17.56 0.2% page out: 10437388 system: 00:37:02.48 2.8% page act: 2124749 IOwait: 00:18:22.53 1.4% page dea: 1094268 hw irq: 00:00:02.33 0.0% page flt: 49002508 sw irq: 00:01:43.26 0.1% swap in : 92170 idle : 18:18:54.53 84.5% swap out: 211122 uptime: 1d 13:51:16.14 context : 76778295 irq 0: 7574027 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 148494 i8042 irq 21: 320127 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 665 ehci_hcd:usb1, uh irq 9: 21965 acpi irq 43: 603641 ahci irq 12: 101096 i8042 irq 44: 32137 eth0 irq 17: 1098 firewire_ohci irq 45: 5971106 i915 irq 18: 0 mmc0 irq 46: 7313791 iwlwifi irq 19: 0 yenta irq 47: 142 snd_hda_intel sda 403526r 166707w eth0 TX 21.17MiB RX 232.58MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 304.36KiB RX 304.36KiB