Ticks for Agda.Primitive max-open-constraints = 0 pointers = 0 pointers (reused) = 0 max-open-metas = 1 metas = 5 equal terms = 9 Ticks for Functor max-open-constraints = 0 pointers = 0 pointers (reused) = 0 max-open-metas = 8 equal terms = 92 unequal terms = 118 metas = 132 Total time 212 ms Parsing 0 ms Import 0 ms Deserialization 0 ms Scoping 16 ms Typing 48 ms Termination 0 ms Termination.RecCheck 0 ms Positivity 0 ms Injectivity 0 ms ProjectionLikeness 0 ms Coverage 0 ms Highlighting 12 ms Serialization 120 ms agda -v0 -v profile:100 misc/Functor.agda -imisc --ignore-interfaces +RTS -slogs/.tmp 107,724,544 bytes allocated in the heap 27,974,912 bytes copied during GC 3,779,240 bytes maximum residency (8 sample(s)) 235,360 bytes maximum slop 11 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 198 colls, 0 par 0.05s 0.05s 0.0002s 0.0007s Gen 1 8 colls, 0 par 0.05s 0.05s 0.0064s 0.0112s INIT time 0.00s ( 0.00s elapsed) MUT time 0.12s ( 0.13s elapsed) GC time 0.10s ( 0.10s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 0.22s ( 0.23s elapsed) %GC time 45.0% (43.1% elapsed) Alloc rate 923,579,893 bytes per MUT second Productivity 54.9% of total user, 52.5% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 3038576 962460 8064 Swap: 13309816 1515524 11794292 Bootup: Fri Mar 21 07:39:37 2014 Load average: 0.87 0.60 0.52 1/539 6398 user : 08:32:10.56 18.0% page in : 16224527 nice : 00:02:58.13 0.1% page out: 27673480 system: 01:45:25.31 3.7% page act: 6401904 IOwait: 00:48:21.96 1.7% page dea: 3950683 hw irq: 00:00:05.33 0.0% page flt: 199297032 sw irq: 00:03:33.09 0.1% swap in : 315805 idle : 1d 12:11:19.66 76.4% swap out: 641953 uptime: 3d 07:52:03.94 context : 191365885 irq 0: 24437292 timer irq 20: 17 ehci_hcd:usb2, uh irq 1: 280062 i8042 irq 21: 752011 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 903682 ehci_hcd:usb1, uh irq 9: 38231 acpi irq 43: 1605298 ahci irq 12: 189974 i8042 irq 44: 65685 eth0 irq 17: 2323 firewire_ohci irq 45: 11775950 i915 irq 18: 0 mmc0 irq 46: 12955971 iwlwifi irq 19: 0 yenta irq 47: 132 snd_hda_intel sda 1116057r 430166w eth0 TX 262.70MiB RX 610.94MiB wlan0 TX 32.05MiB RX 106.06MiB lo TX 731.07KiB RX 731.07KiB