[Agda] Size limit on generated code?

Andreas Abel andreas.abel at ifi.lmu.de
Fri Oct 3 18:29:36 CEST 2014 

On 28.09.2014 11:00, Roly Perera wrote:

 > 1) Are there plans to add IO support to interactive mode (presumably
 > this wouldn't be hard to do via the FFI)?

There are no plans but you might wanna have a go at it.

 > 2) What are the plans for an improved backend? (And is Haskell really
 > a sensible target?)

I started working on a better compiler to Haskell with a student.  Other 
targets might be better, but I have not found a good high-level target 
yet.

 > 3) How supported are the other backends (Epic, JavaScript)?

Currently we have no maintainers for these backends.  We are accepting 
applications... ;-)

 > 4) Is the expectation going forward that Agda will be increasingly
 > used to generate standalone programs, or mainly as a proof assistant?

Well the initial goal was to have a dependently-typed programming 
language, and it is still pursued, but the main effort has been going 
into the front-end and type checker so far.  But see 2).

Cheers,
Andreas

On 28.09.2014 11:00, Roly Perera wrote:
> 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/
> _______________________________________________
> 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/

More information about the Agda mailing list