[Agda] Size limit on generated code?

[Roly Perera]

The 84 LOC example would take some effort to extract into a standalone
program, so I won't attempt that just yet.

After a couple of days of experimentation, I've concluded it's
impractical to compile binaries from my test cases. Compilation takes
up to 30 minutes, and often fails unpredictably with out-of-memory
some chunk of the way through.

My main reason for pursuing standalone binaries in the first place is
that Agda's interactive mode does not seem to support printing to the
console (neither agda -I, nor Emacs mode). I generate output as
strings with embedded newlines and it would be nice to have these
actually printed out, whereas evaluating putStrLn in interactive mode
simply returns a monadic IO.Primitive value (in contrast to GHCi).

So I have some questions now about the Agda roadmap:

1) Are there plans to add IO support to interactive mode (presumably
this wouldn't be hard to do via the FFI)?
2) What are the plans for an improved backend? (And is Haskell really
a sensible target?)
3) How supported are the other backends (Epic, JavaScript)?
4) Is the expectation going forward that Agda will be increasingly
used to generate standalone programs, or mainly as a proof assistant?

thanks,
Roly

On 27 September 2014 20:08, Andreas Abel <abela at chalmers.se> wrote:
> 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/