[Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate

mechvel at scico.botik.ru mechvel at scico.botik.ru
Tue Dec 7 19:37:50 CET 2021


On 2021-12-07 14:10, Nils Anders Danielsson wrote:
> On 2021-12-06 22:01, mechvel at scico.botik.ru wrote:
>> Before installing Agda, I always command (in Linux)
>> 
>>   $ ghc -V
>>   $ which ghc
>> 
>> to see the GHC version and to see where does it reside.
>> I do the same before running `agda' to type-check, and then to compile 
>> my library.
>> Is it possible for another GHC version to intrude?
> 
> If you do not use --with-compiler, then I would assume that Agda just
> calls "ghc".

Today, I moved from  Agda-2.6.2.0.20211129 + ghc-9.2.1
to                   Agda-2.6.2 + ghc-8.8.3.

The same application is built under the same options.
And the latter executable runs 25% faster.

If you are interested, I could send the source to your e-mail
(a preliminary program, not for further distribution).

But this will be about  300K byte,  after I reduce it a bit.
It just multiplies  f * f  where f is a certain large degree univariate 
polynomial
(deg = 2000, 4000 ...),
the coefficient domain is an instance of certain abstract constructions.

--
SM


More information about the Agda mailing list