Martin Escardo
@MartinEscardo@mathstodon.xyz
Professor at the University of Birmingham, UK. I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more. See my meta-blog: https:// cs.bham.ac.uk/~mhe/blog.html
mathstodon.xyz
Martin Escardo
@MartinEscardo@mathstodon.xyz
Professor at the University of Birmingham, UK. I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more. See my meta-blog: https:// cs.bham.ac.uk/~mhe/blog.html
mathstodon.xyz
@MartinEscardo@mathstodon.xyz
·
Apr 07, 2026
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
View full thread on mathstodon.xyz
6
2
0
Conversation (2)
Showing 0 of 2 cached locally.
Syncing comments from the remote thread. 2 more replies are still loading.
Loading comments...