[Agda] Size limit on generated code?

[Andreas Abel]

On 26.09.2014 15:47, flicky frans wrote:
> Could you just forget to close the file?

Well, we could not, even if we wanted to, since MAlonzo writes the whole 
result using writeFile, see

 
https://hackage.haskell.org/package/utf8-string-0.3.8/docs/System-IO-UTF8.html

"Closing files", that makes me nostalgic, that's what you had to do in 
the 1990s programming Pascal...

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

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