ac1 1.7 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152
  1. Ticks for Logic
  2. metas = 5
  3. Ticks for Bool
  4. metas = 70
  5. Ticks for Nat
  6. metas = 21
  7. Ticks for List
  8. attempted-constraints = 7
  9. metas = 57
  10. Ticks for Fin
  11. metas = 79
  12. Ticks for Vec
  13. metas = 71
  14. Ticks for EqProof
  15. metas = 36
  16. Ticks for AC
  17. attempted-constraints = 30
  18. metas = 528
  19. agda -v0 -v profile:100 ac/AC.agda --ignore-interfaces -iac +RTS -slogs/.tmp
  20. 1,065,642,600 bytes allocated in the heap
  21. 139,048,868 bytes copied during GC
  22. 11,573,312 bytes maximum residency (20 sample(s))
  23. 227,084 bytes maximum slop
  24. 30 MB total memory in use (0 MB lost due to fragmentation)
  25. Generation 0: 2006 collections, 0 parallel, 0.24s, 0.25s elapsed
  26. Generation 1: 20 collections, 0 parallel, 0.18s, 0.19s elapsed
  27. INIT time 0.01s ( 0.00s elapsed)
  28. MUT time 1.35s ( 1.36s elapsed)
  29. GC time 0.42s ( 0.43s elapsed)
  30. EXIT time 0.00s ( 0.00s elapsed)
  31. Total time 1.78s ( 1.79s elapsed)
  32. %GC time 23.6% (24.2% elapsed)
  33. Alloc rate 782,638,257 bytes per MUT second
  34. Productivity 75.8% of total user, 75.3% of total elapsed
  35. ──────────────────────────────────────────────────────────────────
  36. Mach kernel version:
  37. Darwin Kernel Version 11.1.0: Tue Jul 26 16:07:11 PDT 2011; root:xnu-1699.22.81~1/RELEASE_X86_64
  38. Kernel configured for up to 8 processors.
  39. 4 processors are physically available.
  40. 8 processors are logically available.
  41. Processor type: i486 (Intel 80486)
  42. Processors active: 0 1 2 3 4 5 6 7
  43. Primary memory available: 8.00 gigabytes
  44. Default processor set: 78 tasks, 333 threads, 8 processors
  45. Load average: 1.24, Mach factor: 6.75