ac1 2.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105
  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 Logic
  9. max-open-constraints = 0
  10. pointers = 0
  11. pointers (reused) = 0
  12. equal terms = 1
  13. max-open-metas = 1
  14. metas = 1
  15. Ticks for Bool
  16. max-open-constraints = 0
  17. pointers = 0
  18. pointers (reused) = 0
  19. max-open-metas = 1
  20. metas = 36
  21. equal terms = 81
  22. Ticks for Nat
  23. max-open-constraints = 0
  24. pointers = 0
  25. pointers (reused) = 0
  26. max-open-metas = 1
  27. metas = 12
  28. equal terms = 32
  29. Ticks for List
  30. pointers = 0
  31. pointers (reused) = 0
  32. max-open-constraints = 2
  33. attempted-constraints = 4
  34. max-open-metas = 4
  35. unequal terms = 20
  36. metas = 32
  37. equal terms = 100
  38. Ticks for Fin
  39. max-open-constraints = 0
  40. pointers = 0
  41. pointers (reused) = 0
  42. max-open-metas = 4
  43. unequal terms = 36
  44. metas = 48
  45. equal terms = 96
  46. Ticks for Vec
  47. max-open-constraints = 0
  48. pointers = 0
  49. pointers (reused) = 0
  50. max-open-metas = 6
  51. unequal terms = 28
  52. metas = 40
  53. equal terms = 74
  54. Ticks for EqProof
  55. max-open-constraints = 0
  56. pointers = 0
  57. pointers (reused) = 0
  58. max-open-metas = 3
  59. unequal terms = 7
  60. metas = 22
  61. equal terms = 42
  62. Ticks for AC
  63. pointers = 0
  64. pointers (reused) = 0
  65. max-open-constraints = 2
  66. attempted-constraints = 14
  67. max-open-metas = 28
  68. metas = 417
  69. unequal terms = 542
  70. equal terms = 572
  71. agda -v0 -v profile:100 ac/AC.agda --ignore-interfaces -iac +RTS -slogs/.tmp
  72. 1,088,776,544 bytes allocated in the heap
  73. 216,653,368 bytes copied during GC
  74. 16,633,488 bytes maximum residency (20 sample(s))
  75. 352,560 bytes maximum slop
  76. 48 MB total memory in use (0 MB lost due to fragmentation)
  77. Tot time (elapsed) Avg pause Max pause
  78. Gen 0 2064 colls, 0 par 0.22s 0.23s 0.0001s 0.0007s
  79. Gen 1 20 colls, 0 par 0.18s 0.21s 0.0103s 0.0311s
  80. INIT time 0.00s ( 0.00s elapsed)
  81. MUT time 0.64s ( 0.65s elapsed)
  82. GC time 0.41s ( 0.43s elapsed)
  83. EXIT time 0.00s ( 0.00s elapsed)
  84. Total time 1.05s ( 1.09s elapsed)
  85. %GC time 38.8% (39.8% elapsed)
  86. Alloc rate 1,699,317,548 bytes per MUT second
  87. Productivity 61.2% of total user, 59.2% of total elapsed
  88. ──────────────────────────────────────────────────────────────────
  89. Mach kernel version:
  90. Darwin Kernel Version 13.0.0: Thu Sep 19 22:22:27 PDT 2013; root:xnu-2422.1.72~6/RELEASE_X86_64
  91. Kernel configured for up to 8 processors.
  92. 4 processors are physically available.
  93. 8 processors are logically available.
  94. Processor type: i486 (Intel 80486)
  95. Processors active: 0 1 2 3 4 5 6 7
  96. Primary memory available: 16.00 gigabytes
  97. Default processor set: 325 tasks, 1532 threads, 8 processors
  98. Load average: 3.90, Mach factor: 4.09