[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