Benchmarking the oksh shell, or, let's look at a lot of C compilers

I love that CompCert is now a thing. Does it perform well compile-time-wise?