syntax1 5.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186
  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 5292 ms
  118. Parsing 44 ms
  119. Import 4 ms
  120. Deserialization 0 ms
  121. Scoping 396 ms
  122. Typing 888 ms
  123. Termination 224 ms
  124. Termination.Graph 24 ms
  125. Termination.RecCheck 12 ms
  126. Termination.Reduce 0 ms
  127. Positivity 280 ms
  128. Injectivity 4 ms
  129. ProjectionLikeness 0 ms
  130. Coverage 116 ms
  131. Highlighting 100 ms
  132. Serialization 3160 ms
  133. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  134. 2,761,990,632 bytes allocated in the heap
  135. 761,771,784 bytes copied during GC
  136. 18,540,552 bytes maximum residency (41 sample(s))
  137. 924,216 bytes maximum slop
  138. 54 MB total memory in use (0 MB lost due to fragmentation)
  139. Tot time (elapsed) Avg pause Max pause
  140. Gen 0 5235 colls, 0 par 1.29s 1.30s 0.0002s 0.0015s
  141. Gen 1 41 colls, 0 par 0.94s 0.94s 0.0229s 0.0453s
  142. INIT time 0.00s ( 0.00s elapsed)
  143. MUT time 3.06s ( 3.12s elapsed)
  144. GC time 2.23s ( 2.24s elapsed)
  145. EXIT time 0.01s ( 0.01s elapsed)
  146. Total time 5.30s ( 5.36s elapsed)
  147. %GC time 42.1% (41.7% elapsed)
  148. Alloc rate 901,462,926 bytes per MUT second
  149. Productivity 57.9% of total user, 57.3% of total elapsed
  150. ──────────────────────────────────────────────────────────────────
  151. Memory: Total Used Free Buffers
  152. RAM: 4001036 3032824 968212 7164
  153. Swap: 13309816 1515524 11794292
  154. Bootup: Fri Mar 21 07:39:37 2014 Load average: 0.72 0.55 0.51 1/542 6348
  155. user : 08:31:51.81 18.0% page in : 16222431
  156. nice : 00:02:58.13 0.1% page out: 27671320
  157. system: 01:45:23.77 3.7% page act: 6401475
  158. IOwait: 00:48:21.42 1.7% page dea: 3950683
  159. hw irq: 00:00:05.33 0.0% page flt: 198980941
  160. sw irq: 00:03:33.03 0.1% swap in : 315805
  161. idle : 1d 12:11:04.08 76.4% swap out: 641953
  162. uptime: 3d 07:51:45.78 context : 191347925
  163. irq 0: 24433934 timer irq 20: 17 ehci_hcd:usb2, uh
  164. irq 1: 280062 i8042 irq 21: 752011 uhci_hcd:usb4, uh
  165. irq 8: 1 rtc0 irq 22: 903682 ehci_hcd:usb1, uh
  166. irq 9: 38231 acpi irq 43: 1604869 ahci
  167. irq 12: 189974 i8042 irq 44: 65534 eth0
  168. irq 17: 2322 firewire_ohci irq 45: 11773676 i915
  169. irq 18: 0 mmc0 irq 46: 12954135 iwlwifi
  170. irq 19: 0 yenta irq 47: 132 snd_hda_intel
  171. sda 1115800r 430000w
  172. eth0 TX 262.70MiB RX 610.92MiB wlan0 TX 32.04MiB RX 106.04MiB
  173. lo TX 731.07KiB RX 731.07KiB