Post #982926

2026-04-07 19:43 UTC

Agda is getting damn fast. In 2019, I asked for a new, fast desktop computer, because running Agda was getting annoying. I don&#39;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 , 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.

Replies (2)

@MartinEscardo@mathstodon.xyz 2026-04-07 20:49

I said: "I don't remember how long the old desktop from 2012 took [in 2019]." I also said: "my 2012 desktop, which I still use, as a server and for casual work, type checks TypeTopology in 4min30sec" Now I've checked the current version of TypeTopology with the 2012 machine using the current version of Agda, namely 2.8.0, and the result is 18m29s Which is way more than the 4m30s I reported above for the development version of Agda. If I were forced to use my 2012 machine for my research, this would be completely feasible now, even though, of course, my M4 giving me 1m15s is more comfortable. Remember that I said it takes 6m30s with an M4 with Agda 2.8.0! So, now, using the development version of Agda in the 2012 machine I take 4m30s, whereas somebody using an M4 takes 6m30m with the released version of Agda. Isn't that amazing? And, remember, too, we don't need to type check everything again every time. @AndrasKovacs @amy

Open ##1330049
@jonmsterling@mathstodon.xyz 2026-04-07 20:01

@MartinEscardo @AndrasKovacs This so amazing… @amy Great work all around!

Open ##1330051