syntax1 2.1 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869
  1. Ticks for Basics
  2. metas = 27
  3. Ticks for Pr
  4. metas = 178
  5. Ticks for Nom
  6. attempted-constraints = 112
  7. metas = 209
  8. Ticks for Kind
  9. metas = 22
  10. Ticks for Cxt
  11. attempted-constraints = 7
  12. metas = 118
  13. Ticks for Loc
  14. attempted-constraints = 39
  15. metas = 224
  16. Ticks for Term
  17. attempted-constraints = 39
  18. metas = 355
  19. Ticks for Shift
  20. attempted-constraints = 28
  21. metas = 269
  22. Ticks for Eta
  23. attempted-constraints = 41
  24. metas = 249
  25. Ticks for Inst
  26. attempted-constraints = 23
  27. metas = 329
  28. Ticks for Subst
  29. attempted-constraints = 34
  30. metas = 267
  31. Ticks for Syntacticosmos
  32. metas = 5
  33. Ticks for UntypedLambda
  34. attempted-constraints = 53
  35. metas = 113
  36. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
  37. 2,504,076,672 bytes allocated in the heap
  38. 372,768,400 bytes copied during GC
  39. 10,912,240 bytes maximum residency (39 sample(s))
  40. 207,564 bytes maximum slop
  41. 30 MB total memory in use (0 MB lost due to fragmentation)
  42. Generation 0: 4715 collections, 0 parallel, 0.72s, 0.73s elapsed
  43. Generation 1: 39 collections, 0 parallel, 0.48s, 0.49s elapsed
  44. INIT time 0.01s ( 0.00s elapsed)
  45. MUT time 3.79s ( 3.81s elapsed)
  46. GC time 1.20s ( 1.22s elapsed)
  47. EXIT time 0.00s ( 0.00s elapsed)
  48. Total time 5.00s ( 5.03s elapsed)
  49. %GC time 24.0% (24.2% elapsed)
  50. Alloc rate 658,587,817 bytes per MUT second
  51. Productivity 75.8% of total user, 75.3% of total elapsed
  52. ──────────────────────────────────────────────────────────────────
  53. Mach kernel version:
  54. Darwin Kernel Version 11.1.0: Tue Jul 26 16:07:11 PDT 2011; root:xnu-1699.22.81~1/RELEASE_X86_64
  55. Kernel configured for up to 8 processors.
  56. 4 processors are physically available.
  57. 8 processors are logically available.
  58. Processor type: i486 (Intel 80486)
  59. Processors active: 0 1 2 3 4 5 6 7
  60. Primary memory available: 8.00 gigabytes
  61. Default processor set: 80 tasks, 346 threads, 8 processors
  62. Load average: 1.26, Mach factor: 6.72