|
1 | 1 | - attributes: |
2 | | - description: stdlib |
3 | | - tags: [stdlib] |
| 2 | + description: Init.Prelude async |
| 3 | + tags: [other] |
4 | 4 | time: &time |
5 | 5 | #runner: time |
6 | 6 | # alternative config: use `perf stat` for extended properties |
|
15 | 15 | "branch-misses", |
16 | 16 | ] |
17 | 17 | rusage_properties: ["maxrss"] |
18 | | - run_config: |
19 | | - <<: *time |
20 | | - cwd: ../../src |
21 | | - cmd: | |
22 | | - set -euxo pipefail |
23 | | - bash -c 'set -eo pipefail; find ${BUILD:-../build/release}/stage3 -name "*.olean" -delete; lakeprof record make -C ${BUILD:-../build/release}/stage3 -j$(nproc) 2>&1 | ../tests/bench/accumulate_profile.py' |
24 | | - lakeprof report -p | awk '{if ($3) cum = $3} END {print "longest build path: " cum}' |
25 | | - lakeprof report -r | awk '{if ($3) cum = $3} END {print "longest rebuild path: " cum}' |
26 | | - max_runs: 2 |
27 | | - parse_output: true |
28 | | - # initialize stage3 cmake + warmup |
29 | | - build_config: |
30 | | - cmd: | |
31 | | - bash -c 'make -C ${BUILD:-../build/release} stage3 -j$(nproc)' |
32 | | -- attributes: |
33 | | - description: stdlib size |
34 | | - tags: [stdlib] |
35 | | - run_config: |
36 | | - cwd: ../../ |
37 | | - cmd: | |
38 | | - set -euxo pipefail |
39 | | - echo -n 'lines: ' |
40 | | - find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 |
41 | | - echo -n 'bytes .olean: ' |
42 | | - find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
43 | | - echo -n 'bytes .olean.server: ' |
44 | | - find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
45 | | - echo -n 'bytes .olean.private: ' |
46 | | - find ${BUILD:-build/release}/stage3/lib/lean -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
47 | | - echo -n 'bytes .ir: ' |
48 | | - find ${BUILD:-build/release}/stage3/lib/lean -name '*.ir' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
49 | | - echo -n 'lines C: ' |
50 | | - find ${BUILD:-build/release}/stage3/lib/temp -name '*.c' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 |
51 | | - echo -n 'lines C++: ' |
52 | | - find src \( -name '*.h' -o -name '*.cpp' \) -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 |
53 | | - echo -n 'max dynamic symbols: ' |
54 | | - find ${BUILD:-build/release}/stage3/lib/lean -name '*.so' -exec bash -c 'nm --extern-only --defined-only {} | wc -l' \; | sort --reverse --numeric-sort | head -n1 |
55 | | - max_runs: 1 |
56 | | - runner: output |
57 | | -- attributes: |
58 | | - description: Init size |
59 | | - tags: [stdlib] |
60 | | - run_config: |
61 | | - cwd: ../../ |
62 | | - cmd: | |
63 | | - set -euxo pipefail |
64 | | - echo -n 'bytes .olean: ' |
65 | | - find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
66 | | - echo -n 'bytes .olean.server: ' |
67 | | - find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean.server' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
68 | | - echo -n 'bytes .olean.private: ' |
69 | | - find ${BUILD:-build/release}/stage3/lib/lean/Init -name '*.olean.private' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 |
70 | | - max_runs: 1 |
71 | | - runner: output |
72 | | -- attributes: |
73 | | - description: libleanshared.so |
74 | | - tags: [stdlib] |
75 | | - run_config: |
76 | | - cmd: | |
77 | | - set -eu |
78 | | - echo -n 'binary size: ' |
79 | | - wc -c ${BUILD:-../../build/release}/stage3/lib/lean/libleanshared.so | cut -d' ' -f 1 |
80 | | - max_runs: 1 |
81 | | - runner: output |
82 | | -- attributes: |
83 | | - description: Init.Prelude async |
84 | | - tags: [other] |
85 | 18 | run_config: |
86 | 19 | <<: *time |
87 | 20 | cwd: ../../src |
|
0 commit comments