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,609,464,048 bytes allocated in the heap
38
405,446,764 bytes copied during GC
39
10,690,544 bytes maximum residency (42 sample(s))
40
219,356 bytes maximum slop
41
28 MB total memory in use (0 MB lost due to fragmentation)
43
Generation 0: 4925 collections, 0 parallel, 1.31s, 1.33s elapsed
44
Generation 1: 42 collections, 0 parallel, 0.96s, 1.00s elapsed
46
INIT time 0.00s ( 0.00s elapsed)
47
MUT time 6.75s ( 6.87s elapsed)
48
GC time 2.27s ( 2.33s elapsed)
49
EXIT time 0.00s ( 0.00s elapsed)
50
Total time 9.02s ( 9.20s elapsed)
52
%GC time 25.2% (25.4% elapsed)
54
Alloc rate 386,740,988 bytes per MUT second
56
Productivity 74.8% of total user, 73.3% 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: 70 tasks, 307 threads, 2 processors
68
Load average: 1.13, Mach factor: 0.86