Agda is getting damn fast.

In 2019, I asked for a new, fast desktop computer, because running Agda was getting annoying.

I don't remember how long the old desktop from 2012 took.

But the 2019 one took 7mins to type check TypeTopology. That was so fast!

And then I got a MacBook Air M1, because they gave one to everyone in our department. At that time, this reduced the time of TypeTopology to 4min, compared to the 7min above.

Now it is 9min in the M1 with the current released version of Agda and TypeTopology, because the latter has grown considerably since 2019/2020.

But guess what! Now my 2012 desktop, which I still use, as a server and for casual work, type checks TypeTopology in 4min30sec, thanks to the work of @AndrasKovacs@mathstodon.xyz , Amy and others.

My oldest machine from 2012 with the development version of Agda outperforms the cutting-edge machines of 2019/2020!

In a Mac M4, the time goes down to 1min15sec. There is no need to desire a Mac M5. A 10% speed up would be peanuts.