[Agda] .agdai weirdness

[Ulf Norell]

On Sun, Mar 2, 2008 at 1:29 PM, Conor McBride <conor at strictlypositive.org>
wrote:

> Hi Ulf
>
> On 2 Mar 2008, at 11:51, Ulf Norell wrote:
> > A tar would be helpful. I'm also curious about what kind of hackery
> > you've been up to :-)
>
> Chalmers just gave me an "illegal attachment" bounce.
> Fair dos. You can download it from here:
>
>   http://strictlypositive.org/Syntacticosmos.tar.gz


It's a stack overflow (i really should do something about that). I don't
know how to (if it's even possible) to increase the stack for the
emacs-mode, but what you can do is use the batch mode to generate the
interface file:

  agda Syntacticosmos.agda +RTS -K32M

After this loading up UntypedLambda works fine in the emacs mode. Of course,
you'll have to repeat the process everytime you change the libraries.

To build the batch tool, if you haven't already, go to src/main and do the
cabal incantations.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080302/b7f831c6/attachment.html