record 3.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081
  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 192 ms
  17. Parsing 4 ms
  18. Import 0 ms
  19. Deserialization 0 ms
  20. Scoping 16 ms
  21. Typing 368 ms
  22. Termination 0 ms
  23. Positivity 4 ms
  24. Injectivity 0 ms
  25. ProjectionLikeness 0 ms
  26. Highlighting 4 ms
  27. Serialization 56 ms
  28. agda -v0 -v profile:100 proj/Record.agda -iproj --ignore-interfaces +RTS -slogs/.tmp
  29. 112,318,584 bytes allocated in the heap
  30. 28,246,320 bytes copied during GC
  31. 4,007,992 bytes maximum residency (8 sample(s))
  32. 241,600 bytes maximum slop
  33. 12 MB total memory in use (0 MB lost due to fragmentation)
  34. Tot time (elapsed) Avg pause Max pause
  35. Gen 0 207 colls, 0 par 0.04s 0.04s 0.0002s 0.0006s
  36. Gen 1 8 colls, 0 par 0.05s 0.05s 0.0065s 0.0123s
  37. INIT time 0.00s ( 0.00s elapsed)
  38. MUT time 0.10s ( 0.10s elapsed)
  39. GC time 0.09s ( 0.09s elapsed)
  40. EXIT time 0.00s ( 0.00s elapsed)
  41. Total time 0.19s ( 0.20s elapsed)
  42. %GC time 46.9% (47.0% elapsed)
  43. Alloc rate 1,111,062,734 bytes per MUT second
  44. Productivity 53.0% of total user, 52.6% of total elapsed
  45. ──────────────────────────────────────────────────────────────────
  46. Memory: Total Used Free Buffers
  47. RAM: 4001036 2698172 1302864 10068
  48. Swap: 13309816 706208 12603608
  49. Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.76 0.39 0.28 1/475 17447
  50. user : 02:24:16.34 10.8% page in : 5178371
  51. nice : 00:02:17.56 0.2% page out: 11110112
  52. system: 00:37:45.78 2.8% page act: 2258133
  53. IOwait: 00:18:36.94 1.4% page dea: 1124086
  54. hw irq: 00:00:02.37 0.0% page flt: 51797466
  55. sw irq: 00:01:44.37 0.1% swap in : 92170
  56. idle : 18:55:49.91 84.7% swap out: 212542
  57. uptime: 1d 14:11:51.54 context : 78045738
  58. irq 0: 7772033 timer irq 20: 10 ehci_hcd:usb2, uh
  59. irq 1: 152327 i8042 irq 21: 323911 uhci_hcd:usb4, uh
  60. irq 8: 1 rtc0 irq 22: 665 ehci_hcd:usb1, uh
  61. irq 9: 22746 acpi irq 43: 608587 ahci
  62. irq 12: 101114 i8042 irq 44: 39694 eth0
  63. irq 17: 1118 firewire_ohci irq 45: 6052223 i915
  64. irq 18: 0 mmc0 irq 46: 7408625 iwlwifi
  65. irq 19: 0 yenta irq 47: 142 snd_hda_intel
  66. sda 404139r 170735w
  67. eth0 TX 21.70MiB RX 237.11MiB wlan0 TX 16.30MiB RX 64.69MiB
  68. lo TX 304.36KiB RX 304.36KiB