syntax1 2.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293
  1. Ticks for Basics
  2. max-open-constraints = 0
  3. max-open-metas = 5
  4. metas = 27
  5. Ticks for Pr
  6. max-open-constraints = 0
  7. max-open-metas = 4
  8. metas = 176
  9. Ticks for Nom
  10. max-open-constraints = 2
  11. max-open-metas = 6
  12. attempted-constraints = 8
  13. metas = 141
  14. Ticks for Kind
  15. max-open-constraints = 0
  16. max-open-metas = 4
  17. metas = 22
  18. Ticks for Cxt
  19. max-open-constraints = 0
  20. max-open-metas = 8
  21. metas = 108
  22. Ticks for Loc
  23. max-open-constraints = 0
  24. max-open-metas = 8
  25. metas = 195
  26. Ticks for Term
  27. max-open-constraints = 2
  28. attempted-constraints = 4
  29. max-open-metas = 10
  30. metas = 315
  31. Ticks for Shift
  32. max-open-constraints = 2
  33. max-open-metas = 14
  34. attempted-constraints = 16
  35. metas = 269
  36. Ticks for Eta
  37. max-open-constraints = 2
  38. attempted-constraints = 12
  39. max-open-metas = 18
  40. metas = 223
  41. Ticks for Inst
  42. max-open-constraints = 2
  43. attempted-constraints = 9
  44. max-open-metas = 16
  45. metas = 329
  46. Ticks for Subst
  47. max-open-constraints = 2
  48. attempted-constraints = 8
  49. max-open-metas = 16
  50. metas = 255
  51. Ticks for Syntacticosmos
  52. max-open-constraints = 0
  53. max-open-metas = 2
  54. metas = 5
  55. Ticks for UntypedLambda
  56. max-open-constraints = 2
  57. attempted-constraints = 20
  58. max-open-metas = 23
  59. metas = 111
  60. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  61. 2,487,596,364 bytes allocated in the heap
  62. 365,934,108 bytes copied during GC
  63. 9,849,836 bytes maximum residency (39 sample(s))
  64. 207,360 bytes maximum slop
  65. 26 MB total memory in use (0 MB lost due to fragmentation)
  66. Generation 0: 4683 collections, 0 parallel, 0.73s, 0.73s elapsed
  67. Generation 1: 39 collections, 0 parallel, 0.46s, 0.47s elapsed
  68. INIT time 0.01s ( 0.00s elapsed)
  69. MUT time 3.90s ( 4.00s elapsed)
  70. GC time 1.19s ( 1.21s elapsed)
  71. EXIT time 0.00s ( 0.00s elapsed)
  72. Total time 5.10s ( 5.20s elapsed)
  73. %GC time 23.3% (23.2% elapsed)
  74. Alloc rate 636,292,016 bytes per MUT second
  75. Productivity 76.5% of total user, 75.0% of total elapsed
  76. ──────────────────────────────────────────────────────────────────
  77. Mach kernel version:
  78. Darwin Kernel Version 11.1.0: Tue Jul 26 16:07:11 PDT 2011; root:xnu-1699.22.81~1/RELEASE_X86_64
  79. Kernel configured for up to 8 processors.
  80. 4 processors are physically available.
  81. 8 processors are logically available.
  82. Processor type: i486 (Intel 80486)
  83. Processors active: 0 1 2 3 4 5 6 7
  84. Primary memory available: 8.00 gigabytes
  85. Default processor set: 89 tasks, 367 threads, 8 processors
  86. Load average: 1.93, Mach factor: 6.06