[Agda] agda halting problem

[Wolfram Kahl]

> On 05.07.2012 18:02, Ondrej Rypacek wrote:
> >Is there a way to tell if Agda is going to halt on my program? It's been 
> >crunching for more than 24 hours now, on a more or less constant memory 
> >use.
> >
> >Is there a way to tell if there's a point in keeping it alive?

Use htop or a similar tool to see how much CPU and memory Agda is using.
If the virtual address space of Agda is larger than your (available) physical memory,
it will be swapping, and probably using on average less than 1% CPU.
In that case, kill Agda.

Are you using

  +RTS -M11G -RTS

? This limits the heap to 11G, which I find a reasonable setting
on a 16G machine where I am also doing other things.
If you shut down X and run Agda from the console and nothing else on that machine,
you can try -M15G.

My command-line invocation normally is:

  +RTS -S -K256M -H11G -M11G -RTS

, using -H to give it the big heap from the start,
-S to see memory use and garbage collection,
-K to give it more stack (whcih I happen to need),
and inside emacs I use (with the development version on an 8G laptop):

Agda2 Program Args: Hide Value
INS DEL String: +RTS
INS DEL String: -K256M
INS DEL String: -H2G
INS DEL String: -M5G
INS DEL String: -RTS
INS


Limiting the heap with -M will make things go through
that without that limit will start swapping.


I suspect that certain syntax errors can make Agda loop (or look like it's looping),
so look out for that first.


If you think your syntax is OK, and Agda is happily using 100% of one core,
leave it running.


On Thu, Jul 05, 2012 at 07:26:20PM +0200, Andreas Abel wrote:
> You could try to profile Agda on your example and see where the runtime 
> goes...

Do that only if your example normally uses significantly less than half of your RAM.
(Observe memory use with -S when running Agda in a terminal or console.)



Wolfram