[Agda] Size limit on generated code?

[flicky frans]

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