[Agda] Possibly infinite/exponential compilation time by just calling a certain function

[Jan Bracker]

Hello,

I have got around the issue of the compilation possibly not terminating by
simply copying the definition of "fca" and "fca'" into the module with the
holes. Now it takes about 40 seconds to compile.

Can anybody explain why just importing these definitions from another
module causes this horrible increase in compilation time? I always thought
separating Agda proofs into several modules was the best way to decrease
compilation time.

Best,
Jan

2017-06-08 12:35 GMT+01:00 Jan Bracker <jan.bracker at googlemail.com>:

> Hello,
>
> I have a module that compiles in a reasonable amount of time with some
> holes in it. If I fill one specific hole using a specific proof from
> another module and start compilation it does not appear to terminate (I
> have let it running for 50+ minutes and it just fills and empties my RAM
> and swap slowly...). Can anyone explain why this happens or how I can get
> around this issue?
>
> The modules with holes can be found here:
>
> https://github.com/jbracker/polymonad-proofs/blob/master/src
> /Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda
>
> On its own this file (with holes) type checks in a reasonable amount of
> time in emacs and if I call Agda directly, as well:
>
> agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Isomorphism
> /Examples/FunctorCompositionAssociator.agda
>
> If I try to fill the hole on line 44 with the expression "fca {ℓC₀} {ℓC₁}
> C" I experience the possibly non-terminating behavior of the type
> checker. As far as I can see that expression exactly matches the type of
> that hole and I don't understand why it is not just accepted immediately.
> As said before I have let Agda work away at the proof for 50+ minutes
> without finishing type checking.
>
> I don't know if this helps at all, but usually when I watch my memory
> usage during Agda compilations t just stepwise allocates memory up to a
> point and then finishes. With the hole filled in the compilation allocates
> and deallocates memory in (2-3 minute) cycles which I have not seen before
> when running Agda. I have not measured memory usage I just watched the
> graph of memory usage in my system monitor while it was running.
>
> "fca" or "functorCompositionAssociator" is imported from
>
> https://github.com/jbracker/polymonad-proofs/blob/master/src
> /Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda
>
> This module on its own again compiles within a reasonable amount of time
> (in emacs and while calling agda directly):
>
> agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Transformat
> ion/Examples/FunctorCompositionAssociator.agda
>
> I first encountered this problem using emacs and I have verified that it
> is actually an Agda and not an emacs issue by calling Agda on the
> respective files directly before and after I replaced the hole with the
> expression.
>
> I have tested this using Agda 2.5.2 built from the Hackage sources on two
> different 64-bit Linux machines (Kubuntu 16.04 & 14.04). The machines have
> 6 / 8 GB of RAM and that is fully used by the compilation together with 2-3
> GB of swap.
>
> So what is causing this issue and how can I get around it?
>
> Best,
> Jan
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170613/b6ce7d92/attachment-0001.html>