syntax1 5.7 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 5048314 μs
  118. Parsing 4000 μs
  119. Import 0 μs
  120. Deserialization 0 μs
  121. Scoping 44003 μs
  122. Typing 180010 μs
  123. Termination 0 μs
  124. Positivity 0 μs
  125. Injectivity 0 μs
  126. ProjectionLikeness 0 μs
  127. Coverage 0 μs
  128. Highlighting 4000 μs
  129. Serialization 452028 μs
  130. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  131. 2,763,798,776 bytes allocated in the heap
  132. 759,495,928 bytes copied during GC
  133. 19,072,496 bytes maximum residency (41 sample(s))
  134. 951,576 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 5236 colls, 0 par 1.24s 1.24s 0.0002s 0.0015s
  138. Gen 1 41 colls, 0 par 0.89s 0.89s 0.0216s 0.0457s
  139. INIT time 0.00s ( 0.00s elapsed)
  140. MUT time 2.92s ( 2.93s elapsed)
  141. GC time 2.13s ( 2.13s elapsed)
  142. EXIT time 0.00s ( 0.00s elapsed)
  143. Total time 5.05s ( 5.06s elapsed)
  144. %GC time 42.1% (42.1% elapsed)
  145. Alloc rate 945,924,360 bytes per MUT second
  146. Productivity 57.9% of total user, 57.8% of total elapsed
  147. ──────────────────────────────────────────────────────────────────
  148. Memory: Total Used Free Buffers
  149. RAM: 4001036 2839324 1161712 28500
  150. Swap: 13309816 737444 12572372
  151. Bootup: Fri Mar 21 07:39:33 2014 Load average: 0.89 0.56 0.44 1/499 20218
  152. user : 02:31:20.34 10.9% page in : 5460427
  153. nice : 00:02:17.68 0.2% page out: 11897848
  154. system: 00:38:40.48 2.8% page act: 2454600
  155. IOwait: 00:19:37.28 1.4% page dea: 1218561
  156. hw irq: 00:00:02.43 0.0% page flt: 55795644
  157. sw irq: 00:01:46.34 0.1% swap in : 93880
  158. idle : 19:39:05.88 84.7% swap out: 221403
  159. uptime: 1d 14:38:19.41 context : 79968774
  160. irq 0: 8042384 timer irq 20: 10 ehci_hcd:usb2, uh
  161. irq 1: 154843 i8042 irq 21: 330828 uhci_hcd:usb4, uh
  162. irq 8: 1 rtc0 irq 22: 670 ehci_hcd:usb1, uh
  163. irq 9: 23761 acpi irq 43: 628259 ahci
  164. irq 12: 101129 i8042 irq 44: 51775 eth0
  165. irq 17: 1143 firewire_ohci irq 45: 6162681 i915
  166. irq 18: 0 mmc0 irq 46: 7531720 iwlwifi
  167. irq 19: 0 yenta irq 47: 153 snd_hda_intel
  168. sda 416046r 178034w
  169. eth0 TX 22.53MiB RX 243.61MiB wlan0 TX 16.30MiB RX 64.69MiB
  170. lo TX 310.84KiB RX 310.84KiB