[Agda] Size limit on generated code?

[Roly Perera]

Thanks Andreas. Running the compiler from the console (rather than
from within Emacs) revealed the string "Killed" being written to the
terminal. I think this essentially means out-of-memory.

Starting from a clean boot, I was able to give Agda enough resources
for it to finish compiling. My test file is 84 lines of Agda and
compiled to 245,323 lines of Haskell (33Mb), but at least it's
well-formed rather than truncated.

Indeed, GHC then managed to compile that source file, generating a
317Mb executable! Which actually works!

Total compilation time was more than 30 minutes, and obviously these
files sizes are kind of ridiculous, but at least we don't have an Agda
bug (as such). I'm guessing there's some kind of quadratic blow up at
play, though, or at least a nasty constant factor arising from all
those coercions..

Roly


On 26 September 2014 14:54, Andreas Abel <abela at chalmers.se> wrote:
> Hi Roly,
>
> I am not aware of any size limit of the MAlonzo compiler.  Please submit an
> issue report with a reproducible test case (can also be a link to a commit
> on github or so) to
>
>   https://code.google.com/p/agda/issues
> .
> Cheers,
> Andreas
>
>
> On 26.09.2014 05:01, Roly Perera wrote:
>>
>> Hi,
>>
>> I've been working on an Agda development for some time and would now
>> like to run some test code. (Outré, I know.) So I'm compiling to a
>> binary using C-c C-x C-c in Emacs.
>>
>> Everything is hunky dory until GHC reaches the .hs file for the test
>> code itself, which appears to be truncated at line 32653. I assume
>> this is some kind of limit on the size of the generated code.
>>
>> I build a test value which represents a pi calculus expression
>> containing several variables. It looks like each occurrence of a de
>> Bruijn index in the pi calculus program is expanding into a rather
>> large amount of Haskell, along these sorts of lines:
>>
>>     (MAlonzo.Code.Data.Fin.d135
>>        (MAlonzo.RTE.mazCoerce
>>           (MAlonzo.Code.Data.Nat.C5
>>              (MAlonzo.RTE.mazCoerce
>>                 (MAlonzo.Code.Data.Nat.mazIntegerToNat
>>                    (8 ::
>>                       Integer)))))
>>        (MAlonzo.RTE.mazCoerce
>>           (MAlonzo.Code.Data.Fin.d135
>>              (MAlonzo.RTE.mazCoerce
>>                 (MAlonzo.Code.Data.Nat.C5
>>                    (MAlonzo.RTE.mazCoerce
>>                       (MAlonzo.Code.Data.Nat.mazIntegerToNat
>>                          (8 ::
>>                             Integer)))))
>>
>> The generated file is truncated in the middle of a token:
>>
>>          (MAlonzo.Code.Dat
>>
>> Is there any way around the limit, if that's indeed what I'm running
>> into, or tips for avoiding this sort of problem?
>>
>> thanks
>> Roly
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda