RE: https://tomkahe.com/@GiftArticles/116245380531611705

"Dear Iranian insurgents: go on in, the water's fine

Your pals,
Israel"

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.

Ukrainian forces shot down a Russian Mi-8 helicopter with in Rostov #Oblast with a deep strike drone, Ukraine's Special Operations Forces (SSO) reported on Nov. 22.

https://kyivindependent.com/ukraine-downs-russian-mi-8-helicopter-with-deep-strike-drone-for-first-time-military-claims/

#Ukraine #Russia

📣 #LeanLang v4.20 has been released! This release brings a total of 346 changes, including feature additions, bug fixes, refactors, documentation improvements and performance improvements, all of which support our Year 2 roadmap: https://lean-fro.org/about/roadmap-y2/

➡️ See the full release notes here: https://lean-lang.org/doc/reference/latest/releases/v4.20.0/#release-v4___20___0