The benchmark action is only run on manual dispatch.
Rationale: this action dramatically slows down CI.
It is nice to run benchmarks, but we don't need them all the time.
We add (non-optimized) testing of benchmark compilation to one of
the CI builds.
