[Agda] MAlonzo performance
Aaron Stump
aaron.stump at gmail.com
Thu Mar 27 19:51:46 CET 2014
I will echo this concern about performance. I am finding for my Agda
parser generator called gratr -- see
https://svn.divms.uiowa.edu/repos/clc/projects/gratr2
with username guest, password guest -- that just getting Agda to
type-check a file a couple thousand lines long takes more time and
memory (10 minutes? more than 4GB?) than is feasible for a development
cycle where you are tweaking your grammar and then compiling so you can
run sample input strings.
I am currently working on contortions so I can get realistic grammars,
which generate Agda files tens of thousands of lines long, through
(hint: type-checking very large strings is instantaneous). But this is
ugly.
Cheers,
Aaron
On Thu 27 Mar 2014 01:07:10 PM CDT, Mateusz Kowalczyk wrote:
> On 27/03/14 17:50, Sergei Meshveliani wrote:
>> Dear Agda developers,
>>
>> this is about the performance of the checker and also of MAlonzo.
>>
>> 1) I have the DoCon library for computer algebra written in Haskell.
>>
>> 2) I have a certain small initial DoCon-A library written in Agda,
>> with proofs provided.
>>
>> The Agda source is somewhat 50 times smaller than the Haskell source of
>> DoCon, about 2 units lower in the used domain constructor level,
>> may be, 300 times smaller in functionality
>> (if not to count proofs!).
>>
>>
>> GHC `makes' DoCon in about 10 minutes, taking about 200 Mb of space.
>>
>> As to DoCon-A,
>> it type-checks within a 9 Gb in 15 min.
>>
>> (this is on the Development Agda of February 16, 2014).
>>
>> Then, there proceeds MAlonzo + GHC, which takes 58 minutes
>> to produce .hs and .o
>> (I put -M9G for space into the $MAlonzo-opt option).
>>
>> There are many modules, and
>> the average .agda size is 20 Kb.
>> the average produced .hs size is 15 Mb.
>>
>> I compile DoCon-A by
>>
>> agda -c $libOpt +RTS ..-M9G ..-RTS $MAlonzo-opt AlgTest.agda
>>
>>
>> To really develop a project, there will be needed to increase the domain
>> level in the .agda code somewhat on 2 units, to increase the module
>> import level on 3-4 units, to add many times more of functionality.
>>
>> And looking forward, I
>>
>> (1) wonder about how could this fit into 12 Gb and, say, 20 hours,
>>
>> (2) recall that fast Integer with proofs is desirable in the Library
>> (represented by macro-digits in N-ary system).
>>
>> About (2):
>> Many things in algorithmic algebra can be computed over
>> (Integer modulo m) rather than Integer, with 1 < m < 20.
>> For example, computing in FiniteField(prime-m) and in constructions
>> over it.
>>
>> Still large Integer cannot be avoided in practice for a long time.
>> It is evident that it can be programmed in Agda with proofs.
>> Probably, it is very difficult to provide proofs for _advanced_
>> algorithms for an arbitrary large integer arithmetic.
>> Therefore, I think, simplest algorithms need to be applied -- for the
>> first release.
>> If it is, say, 10 - 20 times slower on average than in GHC, this will
>> be all right.
>>
>> Regards,
>>
>> ------
>> Sergei
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> I'd like to latch onto this e-mail and ask whether anyone is working on
> improving the size and performance of the generated Haskell code. Even
> mere Hello World in Agda takes ~10 minutes to generate and compile and
> the binary is tens of MBs big. I think this makes the code generation
> very impractical (to not say useless) for toy examples, not to even
> mention actual projects. I mean Sergei is worrying how to get his
> project to take less than 20 hours to compile! Just the thought that 20
> hours is a goal seems silly.
>
> Is MAlonzo intended to ever be practical or is it just a project to show
> that the generation is possible and we don't care for anything else?
>
> Thanks
>
More information about the Agda
mailing list