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 5148 ms Parsing 60 ms Import 12 ms Deserialization 0 ms Scoping 388 ms Typing 768 ms Termination 256 ms Positivity 284 ms Injectivity 0 ms ProjectionLikeness 4 ms Coverage 112 ms Highlighting 104 ms Serialization 3100 ms agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,764,252,584 bytes allocated in the heap 759,797,952 bytes copied during GC 18,500,416 bytes maximum residency (41 sample(s)) 936,344 bytes maximum slop 54 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.26s 1.27s 0.0002s 0.0072s Gen 1 41 colls, 0 par 0.91s 0.92s 0.0224s 0.0445s INIT time 0.00s ( 0.00s elapsed) MUT time 2.98s ( 3.05s elapsed) GC time 2.17s ( 2.19s elapsed) EXIT time 0.00s ( 0.01s elapsed) Total time 5.15s ( 5.24s elapsed) %GC time 42.2% (41.7% elapsed) Alloc rate 929,151,825 bytes per MUT second Productivity 57.8% of total user, 56.9% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 3671720 329316 22688 Swap: 13309816 1087648 12222168 Bootup: Fri Mar 21 07:39:35 2014 Load average: 1.84 0.81 0.43 1/515 21967 user : 05:43:07.52 15.9% page in : 10693471 nice : 00:02:38.83 0.1% page out: 21287076 system: 01:11:21.43 3.3% page act: 4804235 IOwait: 00:33:07.82 1.5% page dea: 2674438 hw irq: 00:00:03.88 0.0% page flt: 167089662 sw irq: 00:02:34.24 0.1% swap in : 123219 idle : 1d 04:19:58.11 79.0% swap out: 347313 uptime: 2d 13:57:53.29 context : 134252925 irq 0: 16692163 timer irq 20: 12 ehci_hcd:usb2, uh irq 1: 250734 i8042 irq 21: 506311 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 26513 ehci_hcd:usb1, uh irq 9: 32803 acpi irq 43: 1101747 ahci irq 12: 187547 i8042 irq 44: 17843 eth0 irq 17: 1831 firewire_ohci irq 45: 8969165 i915 irq 18: 0 mmc0 irq 46: 10184251 iwlwifi irq 19: 0 yenta irq 47: 137 snd_hda_intel sda 720527r 333237w eth0 TX 48.48MiB RX 432.87MiB wlan0 TX 24.08MiB RX 82.43MiB lo TX 558.73KiB RX 558.73KiB