syntax1 5.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183
  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. Total time 5980 ms
  118. Parsing 4 ms
  119. Import 0 ms
  120. Deserialization 0 ms
  121. Scoping 56 ms
  122. Typing 212 ms
  123. Termination 0 ms
  124. Positivity 0 ms
  125. Injectivity 0 ms
  126. ProjectionLikeness 0 ms
  127. Coverage 0 ms
  128. Highlighting 0 ms
  129. Serialization 536 ms
  130. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  131. 2,762,844,552 bytes allocated in the heap
  132. 760,074,864 bytes copied during GC
  133. 18,477,560 bytes maximum residency (41 sample(s))
  134. 950,720 bytes maximum slop
  135. 54 MB total memory in use (0 MB lost due to fragmentation)
  136. Tot time (elapsed) Avg pause Max pause
  137. Gen 0 5235 colls, 0 par 1.48s 1.49s 0.0003s 0.0071s
  138. Gen 1 41 colls, 0 par 1.02s 1.02s 0.0249s 0.0545s
  139. INIT time 0.00s ( 0.00s elapsed)
  140. MUT time 3.49s ( 3.63s elapsed)
  141. GC time 2.49s ( 2.51s elapsed)
  142. EXIT time 0.01s ( 0.01s elapsed)
  143. Total time 5.99s ( 6.15s elapsed)
  144. %GC time 41.6% (40.9% elapsed)
  145. Alloc rate 791,916,986 bytes per MUT second
  146. Productivity 58.4% of total user, 56.9% of total elapsed
  147. ──────────────────────────────────────────────────────────────────
  148. Memory: Total Used Free Buffers
  149. RAM: 4001036 3028544 972492 16872
  150. Swap: 13309816 784388 12525428
  151. Bootup: Fri Mar 21 07:39:33 2014 Load average: 2.75 1.55 0.89 4/539 27862
  152. user : 03:04:02.23 12.3% page in : 7285739
  153. nice : 00:02:38.47 0.2% page out: 13893300
  154. system: 00:45:29.48 3.0% page act: 3079637
  155. IOwait: 00:24:10.42 1.6% page dea: 1689774
  156. hw irq: 00:00:02.78 0.0% page flt: 64627250
  157. sw irq: 00:01:57.68 0.1% swap in : 99438
  158. idle : 20:37:11.47 82.7% swap out: 241354
  159. uptime: 2d 03:33:50.50 context : 91469731
  160. irq 0: 10143519 timer irq 20: 10 ehci_hcd:usb2, uh
  161. irq 1: 161743 i8042 irq 21: 353767 uhci_hcd:usb4, uh
  162. irq 8: 1 rtc0 irq 22: 738 ehci_hcd:usb1, uh
  163. irq 9: 25668 acpi irq 43: 789192 ahci
  164. irq 12: 101297 i8042 irq 44: 62065 eth0
  165. irq 17: 1312 firewire_ohci irq 45: 6640645 i915
  166. irq 18: 0 mmc0 irq 46: 8181891 iwlwifi
  167. irq 19: 0 yenta irq 47: 144 snd_hda_intel
  168. sda 546383r 205196w
  169. eth0 TX 30.30MiB RX 332.57MiB wlan0 TX 16.30MiB RX 64.69MiB
  170. lo TX 360.50KiB RX 360.50KiB