[Agda] Agda mysteriously hangs

[Josh Ko]

Dear Andreas,

Thanks very much! I will try to make a smaller example.

-- JK


On 13 Aug 2010, at 23:04, Andreas Abel wrote:

> 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/
> 
> 
>