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 5048314 μs Parsing 4000 μs Import 0 μs Deserialization 0 μs Scoping 44003 μs Typing 180010 μs Termination 0 μs Positivity 0 μs Injectivity 0 μs ProjectionLikeness 0 μs Coverage 0 μs Highlighting 4000 μs Serialization 452028 μs agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 2,763,798,776 bytes allocated in the heap 759,495,928 bytes copied during GC 19,072,496 bytes maximum residency (41 sample(s)) 951,576 bytes maximum slop 53 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 5236 colls, 0 par 1.24s 1.24s 0.0002s 0.0015s Gen 1 41 colls, 0 par 0.89s 0.89s 0.0216s 0.0457s INIT time 0.00s ( 0.00s elapsed) MUT time 2.92s ( 2.93s elapsed) GC time 2.13s ( 2.13s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 5.05s ( 5.06s elapsed) %GC time 42.1% (42.1% elapsed) Alloc rate 945,924,360 bytes per MUT second Productivity 57.9% of total user, 57.8% of total elapsed ────────────────────────────────────────────────────────────────── Memory: Total Used Free Buffers RAM: 4001036 2839324 1161712 28500 Swap: 13309816 737444 12572372 Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.89 0.56 0.44 1/499 20218 user : 02:31:20.34 10.9% page in : 5460427 nice : 00:02:17.68 0.2% page out: 11897848 system: 00:38:40.48 2.8% page act: 2454600 IOwait: 00:19:37.28 1.4% page dea: 1218561 hw irq: 00:00:02.43 0.0% page flt: 55795644 sw irq: 00:01:46.34 0.1% swap in : 93880 idle : 19:39:05.88 84.7% swap out: 221403 uptime: 1d 14:38:19.41 context : 79968774 irq 0: 8042384 timer irq 20: 10 ehci_hcd:usb2, uh irq 1: 154843 i8042 irq 21: 330828 uhci_hcd:usb4, uh irq 8: 1 rtc0 irq 22: 670 ehci_hcd:usb1, uh irq 9: 23761 acpi irq 43: 628259 ahci irq 12: 101129 i8042 irq 44: 51775 eth0 irq 17: 1143 firewire_ohci irq 45: 6162681 i915 irq 18: 0 mmc0 irq 46: 7531720 iwlwifi irq 19: 0 yenta irq 47: 153 snd_hda_intel sda 416046r 178034w eth0 TX 22.53MiB RX 243.61MiB wlan0 TX 16.30MiB RX 64.69MiB lo TX 310.84KiB RX 310.84KiB