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 224 ms
  17. Parsing 8 ms
  18. Import 0 ms
  19. Deserialization 0 ms
  20. Scoping 12 ms
  21. Typing 496 ms
  22. Termination 4 ms
  23. Positivity 8 ms
  24. Injectivity 0 ms
  25. ProjectionLikeness 0 ms
  26. Coverage 0 ms
  27. Highlighting 4 ms
  28. Serialization 60 ms
  29. agda -v0 -v profile:100 proj/Record.agda -iproj --ignore-interfaces +RTS -slogs/.tmp
  30. 112,519,504 bytes allocated in the heap
  31. 27,007,752 bytes copied during GC
  32. 3,827,200 bytes maximum residency (8 sample(s))
  33. 178,656 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.05s 0.0002s 0.0009s
  37. Gen 1 8 colls, 0 par 0.06s 0.06s 0.0080s 0.0146s
  38. INIT time 0.00s ( 0.00s elapsed)
  39. MUT time 0.12s ( 0.17s elapsed)
  40. GC time 0.10s ( 0.11s elapsed)
  41. EXIT time 0.00s ( 0.00s elapsed)
  42. Total time 0.23s ( 0.28s elapsed)
  43. %GC time 45.6% (38.6% elapsed)
  44. Alloc rate 924,667,662 bytes per MUT second
  45. Productivity 54.3% of total user, 43.7% of total elapsed
  46. ──────────────────────────────────────────────────────────────────
  47. Memory: Total Used Free Buffers
  48. RAM: 4001036 2936860 1064176 17968
  49. Swap: 13309816 784348 12525468
  50. Bootup: Fri Mar 21 07:39:33 2014 Load average: 2.62 1.59 0.91 4/507 27994
  51. user : 03:04:39.29 12.3% page in : 7292595
  52. nice : 00:02:38.47 0.2% page out: 13995304
  53. system: 00:45:33.73 3.0% page act: 3082548
  54. IOwait: 00:24:11.73 1.6% page dea: 1689774
  55. hw irq: 00:00:02.78 0.0% page flt: 65063520
  56. sw irq: 00:01:57.84 0.1% swap in : 99452
  57. idle : 20:37:15.80 82.7% swap out: 241354
  58. uptime: 2d 03:34:14.16 context : 91644972
  59. irq 0: 10148059 timer irq 20: 10 ehci_hcd:usb2, uh
  60. irq 1: 161743 i8042 irq 21: 354101 uhci_hcd:usb4, uh
  61. irq 8: 1 rtc0 irq 22: 738 ehci_hcd:usb1, uh
  62. irq 9: 25668 acpi irq 43: 790202 ahci
  63. irq 12: 101297 i8042 irq 44: 63067 eth0
  64. irq 17: 1312 firewire_ohci irq 45: 6642526 i915
  65. irq 18: 0 mmc0 irq 46: 8183371 iwlwifi
  66. irq 19: 0 yenta irq 47: 144 snd_hda_intel
  67. sda 546876r 205695w
  68. eth0 TX 30.47MiB RX 332.99MiB wlan0 TX 16.30MiB RX 64.69MiB
  69. lo TX 360.50KiB RX 360.50KiB