[Agda] Size limit on generated code?

[Andreas Abel]

Ah, yes, no offense intended. ;-)  I just would be very surprised if a 
package like UTF8 would have a size limit that is anything below the 
size of the address space, like 4GB or so.

Let's wait for a proper bug report before theoretizing more...

On 26.09.2014 20:10, flicky frans wrote:
> While I am agree, that `writeFile` is the best choice for many cases,
> low-level tools are not somewhere in the past.
>
> https://hackage.haskell.org/package/base-4.7.0.1/docs/System-IO.html
>
> There are hClose, hFlush and so on. All mainstream languages have such
> tools. Saying that "closing files" is in 90s is like saying that the
> assembler is in 70s. It all can be useful now.
>
> 2014-09-26 20:35 GMT+04:00, Andreas Abel <abela at chalmers.se>:
>> 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
-- 
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/