record 3.6 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182
  1. Ticks for Agda.Primitive
  2. max-open-constraints = 0
  3. pointers = 0
  4. pointers (reused) = 0
  5. max-open-metas = 1
  6. metas = 5
  7. equal terms = 9
  8. Ticks for Record
  9. max-open-constraints = 0
  10. pointers = 0
  11. pointers (reused) = 0
  12. max-open-metas = 14
  13. equal terms = 160
  14. metas = 174
  15. unequal terms = 254
  16. Total time 184 ms
  17. Parsing 8 ms
  18. Import 0 ms
  19. Deserialization 0 ms
  20. Scoping 8 ms
  21. Typing 400 ms
  22. Termination 0 ms
  23. Positivity 0 ms
  24. Injectivity 0 ms
  25. ProjectionLikeness 0 ms
  26. Coverage 0 ms
  27. Highlighting 12 ms
  28. Serialization 52 ms
  29. agda -v0 -v profile:100 proj/Record.agda -iproj --ignore-interfaces +RTS -slogs/.tmp
  30. 112,522,240 bytes allocated in the heap
  31. 26,989,888 bytes copied during GC
  32. 3,922,512 bytes maximum residency (8 sample(s))
  33. 176,328 bytes maximum slop
  34. 12 MB total memory in use (0 MB lost due to fragmentation)
  35. Tot time (elapsed) Avg pause Max pause
  36. Gen 0 207 colls, 0 par 0.04s 0.04s 0.0002s 0.0010s
  37. Gen 1 8 colls, 0 par 0.05s 0.05s 0.0064s 0.0124s
  38. INIT time 0.00s ( 0.00s elapsed)
  39. MUT time 0.10s ( 0.11s elapsed)
  40. GC time 0.09s ( 0.09s elapsed)
  41. EXIT time 0.00s ( 0.00s elapsed)
  42. Total time 0.19s ( 0.20s elapsed)
  43. %GC time 46.7% (44.6% elapsed)
  44. Alloc rate 1,146,535,532 bytes per MUT second
  45. Productivity 53.2% of total user, 50.2% of total elapsed
  46. ──────────────────────────────────────────────────────────────────
  47. Memory: Total Used Free Buffers
  48. RAM: 4001036 2703360 1297676 8180
  49. Swap: 13309816 748128 12561688
  50. Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.62 0.36 0.36 1/498 22975
  51. user : 02:45:41.40 11.0% page in : 5715275
  52. nice : 00:02:17.68 0.2% page out: 12732952
  53. system: 00:40:58.09 2.7% page act: 2697835
  54. IOwait: 00:20:34.01 1.4% page dea: 1347335
  55. hw irq: 00:00:02.54 0.0% page flt: 59835807
  56. sw irq: 00:01:49.40 0.1% swap in : 94151
  57. idle : 21:10:54.82 84.6% swap out: 224353
  58. uptime: 1d 15:33:20.70 context : 83682409
  59. irq 0: 8685685 timer irq 20: 10 ehci_hcd:usb2, uh
  60. irq 1: 159890 i8042 irq 21: 344251 uhci_hcd:usb4, uh
  61. irq 8: 1 rtc0 irq 22: 670 ehci_hcd:usb1, uh
  62. irq 9: 25306 acpi irq 43: 648528 ahci
  63. irq 12: 101141 i8042 irq 44: 79914 eth0
  64. irq 17: 1194 firewire_ohci irq 45: 6385101 i915
  65. irq 18: 0 mmc0 irq 46: 7719632 iwlwifi
  66. irq 19: 0 yenta irq 47: 153 snd_hda_intel
  67. sda 426034r 187338w
  68. eth0 TX 24.38MiB RX 257.08MiB wlan0 TX 16.30MiB RX 64.69MiB
  69. lo TX 326.70KiB RX 326.70KiB