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 5056 ms
  118. Parsing 64 ms
  119. Import 8 ms
  120. Deserialization 0 ms
  121. Scoping 344 ms
  122. Typing 812 ms
  123. Termination 228 ms
  124. Positivity 304 ms
  125. Injectivity 4 ms
  126. ProjectionLikeness 0 ms
  127. Coverage 112 ms
  128. Highlighting 84 ms
  129. Serialization 3020 ms
  130. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  131. 2,764,293,248 bytes allocated in the heap
  132. 755,940,248 bytes copied during GC
  133. 19,161,328 bytes maximum residency (41 sample(s))
  134. 916,256 bytes maximum slop
  135. 53 MB total memory in use (0 MB lost due to fragmentation)
  136. Tot time (elapsed) Avg pause Max pause
  137. Gen 0 5238 colls, 0 par 1.24s 1.26s 0.0002s 0.0173s
  138. Gen 1 41 colls, 0 par 0.89s 0.90s 0.0219s 0.0462s
  139. INIT time 0.00s ( 0.00s elapsed)
  140. MUT time 2.93s ( 3.00s elapsed)
  141. GC time 2.13s ( 2.16s elapsed)
  142. EXIT time 0.00s ( 0.00s elapsed)
  143. Total time 5.06s ( 5.17s elapsed)
  144. %GC time 42.1% (41.8% elapsed)
  145. Alloc rate 944,527,327 bytes per MUT second
  146. Productivity 57.9% of total user, 56.7% of total elapsed
  147. ──────────────────────────────────────────────────────────────────
  148. Memory: Total Used Free Buffers
  149. RAM: 4001036 2730428 1270608 49632
  150. Swap: 13309816 1231704 12078112
  151. Bootup: Fri Mar 21 07:39:35 2014 Load average: 0.66 0.95 1.08 1/521 23417
  152. user : 06:45:35.68 17.3% page in : 11868467
  153. nice : 00:02:42.68 0.1% page out: 22296072
  154. system: 01:24:15.55 3.6% page act: 4973457
  155. IOwait: 00:39:32.92 1.7% page dea: 2946590
  156. hw irq: 00:00:04.33 0.0% page flt: 171632293
  157. sw irq: 00:02:55.46 0.1% swap in : 258940
  158. idle : 1d 06:03:34.83 77.1% swap out: 492243
  159. uptime: 2d 15:32:39.81 context : 156051732
  160. irq 0: 18586732 timer irq 20: 12 ehci_hcd:usb2, uh
  161. irq 1: 252873 i8042 irq 21: 545875 uhci_hcd:usb4, uh
  162. irq 8: 1 rtc0 irq 22: 903600 ehci_hcd:usb1, uh
  163. irq 9: 36484 acpi irq 43: 1250114 ahci
  164. irq 12: 188270 i8042 irq 44: 540420 eth0
  165. irq 17: 1919 firewire_ohci irq 45: 9511027 i915
  166. irq 18: 0 mmc0 irq 46: 10552410 iwlwifi
  167. irq 19: 0 yenta irq 47: 911 snd_hda_intel
  168. sda 853364r 347285w
  169. eth0 TX 246.53MiB RX 494.39MiB wlan0 TX 24.08MiB RX 82.43MiB
  170. lo TX 580.42KiB RX 580.42KiB