[Agda] Size limit on generated code?

[Andreas Abel]

Haha, these are truly insane numbers!  MAlonzo is beyond salvation, with 
a student I started on a new compiler which does not introduce a 
coercion at *every* node of the Haskell syntax tree.

Still, for the hall of fame, I'd be interested in you 84 line example. 
That would be a very useful benchmark for any new compiler.

Cheers,
Andreas

On 27.09.2014 04:39, Roly Perera wrote:
> 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

-- 
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/