I don't think there's an easy way to check. Not-obviously-terminating definitions will get marked in pink if typechecking completes, but if you go and use one directly in a type somewhere and the definition really doesn't terminate on the input in the type, then the typechecker won't terminate. So if you use possibly non-terminating functions in types, you might want to split up your file to make sure nothing that would normally be pink is hanging your typechecker.<div>
<br></div><div>The other time I've seen things hang is when you use recursive records. You might want to check that you don't have any of those, either.</div><div><br></div><div>Other than that, I don't have too many ideas :(<br>
<br><div class="gmail_quote">On Thu, Jul 5, 2012 at 12:02 PM, Ondrej Rypacek <span dir="ltr"><<a href="mailto:ondrej.rypacek@gmail.com" target="_blank">ondrej.rypacek@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi all<br>
<br>
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.<br>
<br>
Is there a way to tell if there's a point in keeping it alive?<br>
<br>
Cheers,<br>
Ondrej_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>