syntax1 3.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151
  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 Basics
  9. max-open-constraints = 0
  10. pointers = 0
  11. pointers (reused) = 0
  12. max-open-metas = 1
  13. unequal terms = 2
  14. metas = 13
  15. equal terms = 23
  16. Ticks for Pr
  17. max-open-constraints = 0
  18. pointers = 0
  19. pointers (reused) = 0
  20. max-open-metas = 3
  21. unequal terms = 17
  22. metas = 88
  23. equal terms = 172
  24. Ticks for Nom
  25. pointers = 0
  26. pointers (reused) = 0
  27. max-open-constraints = 2
  28. max-open-metas = 4
  29. attempted-constraints = 8
  30. unequal terms = 77
  31. metas = 79
  32. equal terms = 207
  33. Ticks for Kind
  34. max-open-constraints = 0
  35. pointers = 0
  36. pointers (reused) = 0
  37. max-open-metas = 1
  38. metas = 10
  39. equal terms = 20
  40. Ticks for Cxt
  41. max-open-constraints = 0
  42. pointers = 0
  43. pointers (reused) = 0
  44. max-open-metas = 1
  45. unequal terms = 7
  46. metas = 30
  47. equal terms = 157
  48. Ticks for Loc
  49. max-open-constraints = 0
  50. pointers = 0
  51. pointers (reused) = 0
  52. max-open-metas = 6
  53. metas = 130
  54. unequal terms = 145
  55. equal terms = 320
  56. Ticks for Term
  57. pointers = 0
  58. pointers (reused) = 0
  59. max-open-constraints = 2
  60. attempted-constraints = 4
  61. max-open-metas = 10
  62. unequal terms = 140
  63. metas = 243
  64. equal terms = 598
  65. Ticks for Shift
  66. pointers = 0
  67. pointers (reused) = 0
  68. max-open-constraints = 2
  69. max-open-metas = 14
  70. attempted-constraints = 16
  71. metas = 225
  72. unequal terms = 396
  73. equal terms = 639
  74. Ticks for Eta
  75. pointers = 0
  76. pointers (reused) = 0
  77. max-open-constraints = 2
  78. attempted-constraints = 12
  79. max-open-metas = 18
  80. metas = 177
  81. unequal terms = 263
  82. equal terms = 467
  83. Ticks for Inst
  84. pointers = 0
  85. pointers (reused) = 0
  86. max-open-constraints = 2
  87. attempted-constraints = 9
  88. max-open-metas = 16
  89. metas = 263
  90. unequal terms = 538
  91. equal terms = 878
  92. Ticks for Subst
  93. pointers = 0
  94. pointers (reused) = 0
  95. max-open-constraints = 2
  96. attempted-constraints = 8
  97. max-open-metas = 13
  98. metas = 189
  99. unequal terms = 314
  100. equal terms = 537
  101. Ticks for Syntacticosmos
  102. max-open-constraints = 0
  103. pointers = 0
  104. pointers (reused) = 0
  105. max-open-metas = 1
  106. metas = 1
  107. equal terms = 21
  108. Ticks for UntypedLambda
  109. pointers = 0
  110. pointers (reused) = 0
  111. max-open-constraints = 2
  112. attempted-constraints = 20
  113. max-open-metas = 23
  114. metas = 101
  115. unequal terms = 124
  116. equal terms = 180
  117. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  118. 4,425,378,728 bytes allocated in the heap
  119. 915,294,472 bytes copied during GC
  120. 42,370,080 bytes maximum residency (44 sample(s))
  121. 895,816 bytes maximum slop
  122. 100 MB total memory in use (0 MB lost due to fragmentation)
  123. Tot time (elapsed) Avg pause Max pause
  124. Gen 0 8445 colls, 0 par 1.07s 1.08s 0.0001s 0.0011s
  125. Gen 1 44 colls, 0 par 0.73s 0.78s 0.0177s 0.0720s
  126. INIT time 0.00s ( 0.00s elapsed)
  127. MUT time 3.31s ( 3.38s elapsed)
  128. GC time 1.80s ( 1.86s elapsed)
  129. EXIT time 0.00s ( 0.00s elapsed)
  130. Total time 5.12s ( 5.25s elapsed)
  131. %GC time 35.2% (35.5% elapsed)
  132. Alloc rate 1,335,573,905 bytes per MUT second
  133. Productivity 64.8% of total user, 63.2% of total elapsed
  134. ──────────────────────────────────────────────────────────────────
  135. Mach kernel version:
  136. Darwin Kernel Version 13.0.0: Thu Sep 19 22:22:27 PDT 2013; root:xnu-2422.1.72~6/RELEASE_X86_64
  137. Kernel configured for up to 8 processors.
  138. 4 processors are physically available.
  139. 8 processors are logically available.
  140. Processor type: i486 (Intel 80486)
  141. Processors active: 0 1 2 3 4 5 6 7
  142. Primary memory available: 16.00 gigabytes
  143. Default processor set: 327 tasks, 1536 threads, 8 processors
  144. Load average: 3.26, Mach factor: 4.73