[Agda] Agda speed in Ubuntu

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Aug 2 21:17:15 CEST 2019


I accidentally discovered the following (because I booted in an old 
partition to try to find a file, and then kept working on that partition):

A certain Agda file type checks in a core i5 Dell laptop 7th generation

  * In 70 seconds in Ubuntu 18.04 LTS
  * In 50 seconds in Ubuntu 16.04 LTS

I couldn't believe this, and so I tested this in a core i5 HP laptop 6th 
generation. The results where, respectively,

   * 70+delta
   * 50+delta'

with the deltas < 3sec.

Of course we can try to blame the Intel bugs and their fixes for that. 
But, still, both 16.04 and 18.04 are long-term support versions and are 
supposed to incorporate the fixes.

In the four 2x2 cases, Haskell 8.0.2 and Agda 2.6.0.1 are used. Also, in 
both cases nothing else is running in user space.

Can anybody reproduce this?

This is a significant difference: 50/70 is 70% of the time in 16.04. Way 
faster.

Martin


More information about the Agda mailing list