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,605,823,092 bytes allocated in the heap
38
390,477,044 bytes copied during GC
39
10,697,392 bytes maximum residency (41 sample(s))
40
219,300 bytes maximum slop
41
28 MB total memory in use (0 MB lost due to fragmentation)
43
Generation 0: 4906 collections, 0 parallel, 1.38s, 1.40s elapsed
44
Generation 1: 41 collections, 0 parallel, 0.94s, 0.99s elapsed
46
INIT time 0.00s ( 0.00s elapsed)
47
MUT time 6.16s ( 6.23s elapsed)
48
GC time 2.32s ( 2.39s elapsed)
49
EXIT time 0.00s ( 0.00s elapsed)
50
Total time 8.48s ( 8.62s elapsed)
52
%GC time 27.3% (27.7% elapsed)
54
Alloc rate 422,949,899 bytes per MUT second
56
Productivity 72.6% of total user, 71.4% 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: 54 tasks, 201 threads, 2 processors
68
Load average: 1.06, Mach factor: 0.93