[Agda] hot computer churns codata

[Andrés Sicard-Ramírez]

2009/5/20 Conor McBride <conor at strictlypositive.org>:
>
>Now that's funny! Thanks very much!

You are welcome!
(Although, from an Alan Turing's biography, I have the idea that the
previous sentence is not very British :-) )

>
> Many thanks. (This command line thing: is it a recent return
> to the old ways?

I don't think so. I use the command line when I have some memory
issues (see below).


>
> (Hmm. I just tried --no-termination-check under emacs and
> got a stack overflow after about 5 minutes.)

I had the same problem. If we increase the stack for ghci and we run
the "emacs interface by hand", the file is type checked

$ ghci +RTS -K20m
Prelude>  :set -package Agda-2.2.3
Prelude>  :mod + Agda.Interaction.GhciTop
Prelude Agda.Interaction.GhciTop>  cmd_load "/tmp/MTypes.agda" ["."]
Checking /tmp/MTypes.agda.
agda2_mode_code (agda2-highlight-reload)
agda2_mode_code (agda2-annotate '(0))
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-info-action
                 "*All Goals*"
                 "?0 : (S : U) (T : U) (Q : El (Prf (S <-> T))) (s : El S) →
El (Prf (eq S s T (coe S T Q s)))
")


I don't know how change the stack for ghci inside Agda. In a previous
version of the Agda emacs mode, I changed in the file agda2-mode.el

(haskell-ghci-start-process nil)

by

(haskell-ghci-start-process t)

and I could set up a different stack for ghci. However, it seems don't
work with the current version.


BTW, I have had some problems with stack overflows too, and following
Ulf's advice I replaced some implicit arguments by explicit ones and
this solved my problems.

>
>> $ time agda --no-termination-check MTypes.agda
>> Checking /tmp/MTypes.agda.
>>
>> Unsolved metas at the following locations:
>>  /tmp/MTypes.agda:273,9-13
>
> That's fair -- there's a hole because I can't have a postulate
> in a mutual block,

I didn't know this restriction. Do you know why?

Best,

-- 
Andrés