Martin Escardo

When the Mac M1 was released, and offered at our university, it was great.

Type checking TypeTopology went down from 7min to 4min, compared to the previous (quite recent at that time) Intel machine I had.

That was great!

But then, of course, TypeTopology keeps growing, and, currently, with an M4 machine, it takes 6min to type check.

But then come three developments since the current version of Agda, in the development version.

One is to make things sequentially faster, which brings the time down to 4:30min from the previous 6min.

And then, in parallel, using the new `-j` option, down to 2:20min.

And then, with a better handling of mutual blocks, even faster. That I can't measure yet, but for one particular module it goes down from 20secs to 4sec.

These three things make everything so much faster.

You don't need to buy new cutting-edge hardware. You just need better algorithms to beat the next generation of hardware.

Thanks, Agda developers, for investing your time on that!

From 6min down to to 2:20min is rather impressive. It is much better than what Apple can offer when moving from M4 to M5.

Added in proof. Save the planet with better algorithms.

Mar 7 at 5:00pmWeb
Show threadzwarichMar 7
@MartinEscardo What’s the actual change to mutual block handling?
Show threadAndrasKovacsMar 7

@zwarich @MartinEscardo For positivity checking we need to check how definitions and arguments occur in definitions. We do this for a mutual block at once. The old code used a naive cubic transitive closure of the occurrence graph. The new code is a quadratic depth-first search that's more specific for the work and also more optimized.

https://github.com/agda/agda/commit/4e481bf79340e0e58a99818e20dbf377d1acae90

Remove transitive closure from positivity checking (#8445) · agda/agda@4e481bf

Replace transitive closure computation with depth-first search in positivity checking. The former is supposed to be cubic while the new version is quadratic. It seems to be much faster in practice ...

GitHub
Show threadReed MullanixMar 8
@MartinEscardo Im glad that the performance work is appreciated!
Show threadsoaprootMar 8
@MartinEscardo Ooh nice, I always thought Metamath would have the speed records (for reasons I could go into but won't try to here). But these numbers, for all of TypeTopology, are quite respectable.
Show threadNamdak TönpaMar 11
@MartinEscardo According to that style of thinking and logic it applies Agda should be deleted and rewritten as poorly designed and bad written software. Possibly inconsistent.
Show threadNamdak TönpaMar 11
@MartinEscardo I just don't understand why I should wait when you fix Agda when I can write any type checker and work within its theory in order to be published? Why I should feel than pain with Agda? This is science monopoly and corruption.
Show threadNamdak TönpaMar 11
@MartinEscardo Agda is the worst proving system by speed and you know it.
Show threadNamdak TönpaMar 11
@MartinEscardo I encourage every single thinking person to reevaluate its usage.
Show threadMartin EscardoMar 11

For public disclosure, I am blocking this person from my feed, because their remarks are not conductive to progress, let alone conductive to a sense of community.

@5ht