[Agda] Size limit on generated code?

[flicky frans]

Could you just forget to close the file?

2014-09-26 10:54 GMT+04:00, Andreas Abel <abela at chalmers.se>:
> 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
>