6
attempted-constraints = 104
11
attempted-constraints = 6
14
attempted-constraints = 36
17
attempted-constraints = 36
20
attempted-constraints = 24
23
attempted-constraints = 39
26
attempted-constraints = 21
29
attempted-constraints = 30
31
Ticks for Syntacticosmos
33
Ticks for UntypedLambda
34
attempted-constraints = 48
36
../src/main/dist/build/agda/agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp
37
2,514,579,624 bytes allocated in the heap
38
367,574,424 bytes copied during GC
39
11,060,416 bytes maximum residency (40 sample(s))
40
249,176 bytes maximum slop
41
30 MB total memory in use (0 MB lost due to fragmentation)
43
Generation 0: 4733 collections, 0 parallel, 1.29s, 1.32s elapsed
44
Generation 1: 40 collections, 0 parallel, 0.90s, 0.95s elapsed
46
INIT time 0.00s ( 0.00s elapsed)
47
MUT time 5.89s ( 6.04s elapsed)
48
GC time 2.19s ( 2.27s elapsed)
49
EXIT time 0.00s ( 0.00s elapsed)
50
Total time 8.09s ( 8.31s elapsed)
52
%GC time 27.1% (27.3% elapsed)
54
Alloc rate 426,591,894 bytes per MUT second
56
Productivity 72.9% of total user, 70.9% of total elapsed
58
──────────────────────────────────────────────────────────────────
60
Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
61
Kernel configured for up to 2 processors.
62
2 processors are physically available.
63
2 processors are logically available.
64
Processor type: i486 (Intel 80486)
65
Processors active: 0 1
66
Primary memory available: 2.00 gigabytes
67
Default processor set: 66 tasks, 254 threads, 2 processors
68
Load average: 1.37, Mach factor: 0.87