ac1 2.7 KB

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798
  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. agda -v0 -v profile:100 ac/AC.agda --ignore-interfaces -iac +RTS -slogs/.tmp (null)
  65. 546,340,820 bytes allocated in the heap
  66. 95,433,004 bytes copied during GC
  67. 9,376,172 bytes maximum residency (16 sample(s))
  68. 190,924 bytes maximum slop
  69. 27 MB total memory in use (0 MB lost due to fragmentation)
  70. Tot time (elapsed) Avg pause Max pause
  71. Gen 0 1028 colls, 0 par 0.25s 0.29s 0.0003s 0.0317s
  72. Gen 1 16 colls, 0 par 0.21s 0.25s 0.0154s 0.0502s
  73. INIT time 0.00s ( 0.00s elapsed)
  74. MUT time 0.90s ( 0.97s elapsed)
  75. GC time 0.46s ( 0.54s elapsed)
  76. EXIT time 0.00s ( 0.00s elapsed)
  77. Total time 1.37s ( 1.51s elapsed)
  78. %GC time 33.8% (35.6% elapsed)
  79. Alloc rate 604,580,681 bytes per MUT second
  80. Productivity 66.2% of total user, 59.8% of total elapsed
  81. ──────────────────────────────────────────────────────────────────
  82. Mach kernel version:
  83. Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
  84. Kernel configured for up to 2 processors.
  85. 2 processors are physically available.
  86. 2 processors are logically available.
  87. Processor type: i486 (Intel 80486)
  88. Processors active: 0 1
  89. Primary memory available: 2.00 gigabytes
  90. Default processor set: 112 tasks, 508 threads, 2 processors
  91. Load average: 1.38, Mach factor: 0.81