[Agda] hot computer churns codata
andres.sicard.ramirez at gmail.com
Wed May 20 15:46:15 CEST 2009
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" ["."]
agda2_mode_code (agda2-annotate '(0))
agda2_mode_code (agda2-status-action "")
"?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
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:
> 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?
More information about the Agda