[Agda-dev] travis errors

[Ulf Norell]

I did some refactoring of TypeChecking.Substitute, breaking out a couple of
modules. Hopefully this will alleviate the Travis problems.

/ Ulf

On Tue, Oct 25, 2016 at 2:33 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/20161031/a2f2847e/attachment.html