<div dir="ltr">Hello,<div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Best,</div><div>Jan <br><div class="gmail_extra"><br><div class="gmail_quote">2017-06-08 12:35 GMT+01:00 Jan Bracker <span dir="ltr"><<a href="mailto:jan.bracker@googlemail.com" target="_blank">jan.bracker@googlemail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hello,<div><br></div><div>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?</div><div><br></div><div>The modules with holes can be found here:</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/master/src/Theory/Natural/Isomorphism/Examples/FunctorCompositionAssociator.agda" target="_blank">https://github.com/jbracker/po<wbr>lymonad-proofs/blob/master/src<wbr>/Theory/Natural/Isomorphism/Ex<wbr>amples/FunctorCompositionAssoc<wbr>iator.agda</a><br></div><div><br></div><div>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:</div><div><br></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)">agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Isomorphism<wbr>/Examples/FunctorCompositionAs<wbr>sociator.agda</span><br></span></div><div><br></div><div>If I try to fill the hole on line 44 with the expression "<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">fca {ℓC₀} {ℓC₁} C</span>" 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. </div><div><br></div><div>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.</div><div><br></div><div>"<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">fca</span>" or "<span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">functorCompositionAssociator</span>" is imported from</div><div><br></div><div><a href="https://github.com/jbracker/polymonad-proofs/blob/master/src/Theory/Natural/Transformation/Examples/FunctorCompositionAssociator.agda" target="_blank">https://github.com/jbracker/po<wbr>lymonad-proofs/blob/master/src<wbr>/Theory/Natural/Transformation<wbr>/Examples/FunctorCompositionAs<wbr>sociator.agda</a><br></div><div><br></div><div>This module on its own again compiles within a reasonable amount of time (in emacs and while calling agda directly):</div><div><br></div><div><span style="font-family:monospace"><span style="color:rgb(0,0,0)">agda -isrc -v 0 +RTS -K40m -RTS src/Theory/Natural/Transformat<wbr>ion/Examples/FunctorCompositio<wbr>nAssociator.agda</span><br></span></div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>So what is causing this issue and how can I get around it?<br></div><div><br></div><div>Best,</div><div>Jan</div></div>
</blockquote></div><br></div></div></div>