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 188 ms
  17. Parsing 4 ms
  18. Import 0 ms
  19. Deserialization 0 ms
  20. Scoping 12 ms
  21. Typing 352 ms
  22. Termination 0 ms
  23. Positivity 8 ms
  24. Injectivity 4 ms
  25. ProjectionLikeness 0 ms
  26. Coverage 0 ms
  27. Highlighting 8 ms
  28. Serialization 68 ms
  29. agda -v0 -v profile:100 proj/Record.agda -iproj --ignore-interfaces +RTS -slogs/.tmp
  30. 112,633,712 bytes allocated in the heap
  31. 28,693,160 bytes copied during GC
  32. 3,890,784 bytes maximum residency (8 sample(s))
  33. 238,352 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 208 colls, 0 par 0.04s 0.04s 0.0002s 0.0006s
  37. Gen 1 8 colls, 0 par 0.05s 0.05s 0.0065s 0.0119s
  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 47.2% (44.1% elapsed)
  44. Alloc rate 1,140,037,613 bytes per MUT second
  45. Productivity 52.7% of total user, 49.2% of total elapsed
  46. ──────────────────────────────────────────────────────────────────
  47. Memory: Total Used Free Buffers
  48. RAM: 4001036 2736452 1264584 21328
  49. Swap: 13309816 803944 12505872
  50. Bootup: Fri Mar 21 07:39:33 2014 Load average: 1.19 0.96 0.56 2/496 6951
  51. user : 04:05:33.77 13.1% page in : 8331195
  52. nice : 00:02:38.49 0.1% page out: 17485384
  53. system: 00:56:03.67 3.0% page act: 3949990
  54. IOwait: 00:27:58.88 1.5% page dea: 2045139
  55. hw irq: 00:00:03.18 0.0% page flt: 146457361
  56. sw irq: 00:02:12.00 0.1% swap in : 106250
  57. idle : 1d 01:44:46.11 82.2% swap out: 259206
  58. uptime: 2d 06:47:25.47 context : 106559368
  59. irq 0: 12397368 timer irq 20: 10 ehci_hcd:usb2, uh
  60. irq 1: 177351 i8042 irq 21: 413556 uhci_hcd:usb4, uh
  61. irq 8: 1 rtc0 irq 22: 738 ehci_hcd:usb1, uh
  62. irq 9: 25668 acpi irq 43: 916234 ahci
  63. irq 12: 101402 i8042 irq 44: 144018 eth0
  64. irq 17: 1493 firewire_ohci irq 45: 7456797 i915
  65. irq 18: 0 mmc0 irq 46: 8901437 iwlwifi
  66. irq 19: 0 yenta irq 47: 144 snd_hda_intel
  67. sda 606585r 268790w
  68. eth0 TX 36.64MiB RX 379.67MiB wlan0 TX 16.30MiB RX 64.69MiB
  69. lo TX 382.48KiB RX 382.48KiB