[Agda] agda halting problem

[Daniel Peebles]

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.

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.

Other than that, I don't have too many ideas :(

On Thu, Jul 5, 2012 at 12:02 PM, Ondrej Rypacek <ondrej.rypacek at gmail.com>wrote:

> Hi all
>
> 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?
>
> Cheers,
> Ondrej_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120705/3dfea259/attachment.html