[Agda] Agda mysteriously hangs

[Andreas Abel]

Hi Josh,

strange indeed.  I ran through you file DTerm.agda with --no- 
termination-check and dummy commented out.  With verbosity 7 (-v 7),  
Agda seems to hang after outputting

Building interface...
   instantiating all meta variables
   interface complete

Looking at the code

   Interaction/Imports.hs , end of function createInterface

I see

     if and [ null termErrs, null unsolvedMetas, null  
unsolvedConstraints ]
      then do
       -- The file was successfully type-checked (and no warnings were
       -- encountered), so the interface should be written out.
       t <- writeInterface (filePath $ toIFile file) i
       return (i, Right t)

so it is likely that "writeInterface", which is not called if there  
were termination errors or unsolved goals, takes either insanely long  
or loops.

Btw., I realized that already type and termination checking take long  
for DTerm since function "abs" has lots of auxiliary functions  
generated by with, rewrite, and \sharp.

Please try to reproduce the behavior with a smaller example (best:  
minimal example) and submit it as an issue to our bugtracker at  
code.google.com.

Cheers,
Andreas

On Aug 11, 2010, at 11:29 AM, Josh Ko wrote:

> Hi,
>
> We have been working on encoding concurrent processes with simple
> session types in Agda, and come up with a datatype for coinductive
> process terms, which is heavily indexed with typing contexts. We
> have followed the locally nameless approach [1], which means there
> are both free and bound channels, represented by strings and (safe)
> de Bruijn indices respectively. One key operation is abstracting
> a free channel to a bound channel, whose implementation requires
> a lot of typecasts (rewrites) all through the code and is hard to
> be put into a form of guarded recursion (our process terms are
> coinductive). We decided to turn off the termination checker at
> least for the moment, so we can carry on to some other proofs.
> The strange thing is: if we do not add
>
>  {-# OPTIONS --no-termination-check #-}
>
> at the top of the file, then the typechecker stops and the function
> is highlighted as non-terminating, which is expected. If the option
> is turned on, however, the typechecker just hangs. Now if one leaves
> any hole in the file (with the option still turned on), say appending
>
>  dummy : ℕ
>  dummy = {!!}
>
> at the end, then the typechecker stops again. Is there an explanation
> for this phenomenon? I have put the relevant files at
>
>  http://w.csie.org/~b94087/EvenMoreHeavilyIndexedSyntaxRevisited/
>
> and the problematic function is called abs in the file DTerm.agda,
> which can take a long time to load even if the --no-termination-check
> option is off or a hole is left. The version of Agda is the most
> recent development version pulled from the darcs repository.
>
> Thanks!
>
> -- JK
>
>
> [1] Aydemir et al. Engineering Formal Metatheory. POPL '08.
>    http://doi.acm.org/10.1145/1328438.1328443_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/