[Agda] Agda speed in Ubuntu

Guillaume Brunerie guillaume.brunerie at gmail.com
Fri Aug 30 14:34:27 CEST 2019


Did you try the following instead, to get the info Nils is asking for
(i.e. without the "-2.6.0.1" suffix)?

$ ghc-pkg describe Agda

This is what is needed on my machine, at least.

Best,
Guillaume

Den ons 28 aug. 2019 kl 21:45 skrev Martin Escardo <m.escardo at cs.bham.ac.uk>:
>
> FYI, If one installs ghc-8.6.5 from ppa:hvr/ghc in Ubuntu 18.04, one
> gets the same type checking time as in 16.04 after reinstalling Agda. Martin
>
> On 02/08/2019 20:17, Martin Escardo wrote:
> > 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
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list