[Agda-dev] travis errors

[Ulf Norell]

Clearly the problems started when you fixed the capitalization of deBruijn
(or possibly the patch that added the Subst instance for levels). It might
be that that just pushed memory requirements over the edge.

/ Ulf

On Mon, Oct 24, 2016 at 8:41 AM, Andreas Abel <abela at chalmers.se> wrote:

> Recently travis tests 4 and 2 for agda/agda error a lot, usually going out
> of memory at Agda.TypeChecking.Substitute.
>
> [134 of 330] Compiling Agda.TypeChecking.Substitute (
> src/full/Agda/TypeChecking/Substitute.hs, .stack-work/dist/x86_64-linux/
> Cabal-1.24.0.0/build/Agda/TypeChecking/Substitute.o )
>
> --  While building package Agda-2.5.2 using:
>
>
> /home/travis/build/agda/agda/.stack-work/dist/x86_64-linux/Cabal-1.24.0.0/setup/setup
> --builddir=.stack-work/dist/x86_64-linux/Cabal-1.24.0.0 build lib:Agda
> exe:agda exe:agda-ghc-names exe:agda-mode --ghc-options " -ddump-hi
> -ddump-to-file"
>
>     Process exited with code: ExitFailure (-9) (THIS MAY INDICATE OUT OF
> MEMORY)
>
> Something seems to require a lot of memory here which it did not use
> before. What is the size of the file created by -ddump-hi?
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20161025/635ab882/attachment.html