build bot details

Stream: CI

[Gabriel Ebner]

@Jannis Limperg Can you give some details on the benchmarking system? From the Azure dashboard, I can see that you're an E4as v4 VM. How is Lean executed? That is, do you compile each file individually or do you run lean --make? Do you make use of parallelism (the VM has "four" "cores")? (I didn't see this mentioned anywhere.)

[Jannis Limperg]

The benchmark runner runs this Docker container with

docker run jlimperg/mathlib-bench-runner daemon runner1 https://mathlib-bench.limperg.de <secret>

If you want comparable timings, you could pull this container on the same VM and do

docker run jlimperg/mathlib-bench-runner oneshot <commit> --runs N

Source code for the container is here; the runner's main is in this file.

Internally, the runner runs

leanpkg build -- --threads 4 --memory 20000

for the full build. Then it does another build for the per-file timings with

lean -j0 <file>

for each file (using the oleans from the full build).

Actually, I discovered that the runner was misconfigured for a while and ran the full build with --threads 16. I'm currently testing whether that makes a difference.

[Gabriel Ebner]

Thanks! The code looks much more professional than our typical benchmarking scripts! :love: One thing I'm still not clear about: is the 2h30m the time that leanpkg build -- --threads 16 --memory 20000 takes or is the whole benchmarking run (incl. per-file benchmarks)?

[Jannis Limperg]

Thanks! The reported time is only leanpkg build; the per-file run is only used for the per-file timings.