ac2 2.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106
  1. Ticks for Logic
  2. max-open-constraints = 0
  3. pointers = 0
  4. pointers (reused) = 0
  5. equal terms = 1
  6. max-open-metas = 1
  7. metas = 1
  8. Ticks for Bool
  9. max-open-constraints = 0
  10. pointers = 0
  11. pointers (reused) = 0
  12. max-open-metas = 1
  13. metas = 36
  14. equal terms = 81
  15. Ticks for Nat
  16. max-open-constraints = 0
  17. pointers = 0
  18. pointers (reused) = 0
  19. max-open-metas = 1
  20. metas = 12
  21. equal terms = 32
  22. Ticks for List
  23. pointers = 0
  24. pointers (reused) = 0
  25. max-open-constraints = 2
  26. attempted-constraints = 4
  27. max-open-metas = 4
  28. unequal terms = 20
  29. metas = 32
  30. equal terms = 100
  31. Ticks for Fin
  32. max-open-constraints = 0
  33. pointers = 0
  34. pointers (reused) = 0
  35. max-open-metas = 4
  36. unequal terms = 36
  37. metas = 48
  38. equal terms = 96
  39. Ticks for Vec
  40. max-open-constraints = 0
  41. pointers = 0
  42. pointers (reused) = 0
  43. max-open-metas = 6
  44. unequal terms = 28
  45. metas = 40
  46. equal terms = 74
  47. Ticks for EqProof
  48. max-open-constraints = 0
  49. pointers = 0
  50. pointers (reused) = 0
  51. max-open-metas = 3
  52. unequal terms = 7
  53. metas = 22
  54. equal terms = 42
  55. Ticks for AC
  56. pointers = 0
  57. pointers (reused) = 0
  58. max-open-constraints = 2
  59. attempted-constraints = 14
  60. max-open-metas = 28
  61. metas = 417
  62. unequal terms = 540
  63. equal terms = 570
  64. Ticks for Example
  65. max-open-constraints = 0
  66. pointers = 0
  67. pointers (reused) = 0
  68. max-open-metas = 7
  69. unequal terms = 68
  70. metas = 83
  71. equal terms = 342
  72. agda -v0 -v profile:100 ac/Example.agda --ignore-interfaces -iac +RTS -slogs/.tmp (null)
  73. 688,736,936 bytes allocated in the heap
  74. 108,268,464 bytes copied during GC
  75. 8,266,056 bytes maximum residency (19 sample(s))
  76. 270,544 bytes maximum slop
  77. 23 MB total memory in use (0 MB lost due to fragmentation)
  78. Tot time (elapsed) Avg pause Max pause
  79. Gen 0 1297 colls, 0 par 0.30s 0.33s 0.0003s 0.0075s
  80. Gen 1 19 colls, 0 par 0.23s 0.26s 0.0138s 0.0433s
  81. INIT time 0.00s ( 0.00s elapsed)
  82. MUT time 1.16s ( 1.20s elapsed)
  83. GC time 0.53s ( 0.59s elapsed)
  84. EXIT time 0.00s ( 0.00s elapsed)
  85. Total time 1.69s ( 1.80s elapsed)
  86. %GC time 31.4% (33.0% elapsed)
  87. Alloc rate 595,978,796 bytes per MUT second
  88. Productivity 68.6% of total user, 64.4% of total elapsed
  89. ──────────────────────────────────────────────────────────────────
  90. Mach kernel version:
  91. Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
  92. Kernel configured for up to 2 processors.
  93. 2 processors are physically available.
  94. 2 processors are logically available.
  95. Processor type: i486 (Intel 80486)
  96. Processors active: 0 1
  97. Primary memory available: 2.00 gigabytes
  98. Default processor set: 112 tasks, 505 threads, 2 processors
  99. Load average: 1.23, Mach factor: 0.76