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

[Wolfram Kahl]

On Tue, Jun 27, 2017 at 04:09:09PM +0100, Jan Bracker wrote:
> I tried to add the last postulate I need, but even though I now have marked
> all of the proofs as abstract the compilation time is again at 30+ minutes
> with no end in sight:
> 
> https://github.com/jbracker/polymonad-proofs/blob/ec730f224eedb478cfdfb277c7eea2503dae5771/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates/PentagonId.agda

Have you tried installing a version of Agda with Andrea Vezzosi's patch from
  https://github.com/agda/agda/issues/1625#issuecomment-132196576
applied?
(You also need a separate installation of the standard library,
 and either work in a separate clone of your repository,
 or delete all .agdai files before you switch either way.
 To make this manageable, change the Agda version in the .cabal file
 before the patched installation; my patched version of 2.5.2 is 2.5.2.0.1.
 That version number also needs to be changed in:
    src/agda/src/data/emacs-mode/agda2-mode.el
)


Wolfram

P.S.: Afterthought: If you are not restricting the heap of Agda by
      running agda with, e.g., +RTS -M13G -RTS on your 16G machine,
      then agda may be using a heap that does not fit into your RAM,
      and swaps without end --- kill it, because it does not make
      sufficient progress. ``htop'' is your friend.
      I recommend at most
        +RTS -M11G -H11G -A256M -S -RTS
      if you are also using that 16G machine for daily life.