segfault in Data.HashTable, triggered by long Agda runs

[wkahl]

Agda uses Data.HashTable for interface (*.agdai) serialisation.

I have been able to localise a reproducible segfault (with one of the many theories in a sizeable Agda develoment) in Agda.TypeChecking.Serialise.encode inside the icode call, which essentially limits the possible source of the segfault to the Agda module Agda.TypeChecking.Serialise and to Data.HashTable.

Then I replaced all hash table uses in encode with Data.Map, and the Agda run in question finishes successfully. (I confirmed with a selection of the theories that already could be type-checked with Data.HashTable that the {{Data.Map}}}-based version generates the same interface files.)

(Agda interface serialisation maintains four partial maps; their respective sizes at the end of this run are 151796,733,3319,0.)

I consider this as a (non-constructive) proof that there is a bug in Data.HashTable.

(For the time being, I need to make some long-delayed progress in my Agda developments and won't have time to try to debug Data.HashTable, but I should be able to occasionally test potential fixes.)

Wolfram

[wkahl]

Currently, I normally run with the following RTS flags:

 +RTS -C0 -i0 -K64M -M12G -H12G -S -RTS 

[simonmar]

Can you give us instructions to reproduce the problem, even if it involves compiling Agda?

[simonpj]

Which version of GHC was this? There was a bug in 6.12 which seg-faulted sometimes with very large heaps. We can't make progress on this without more info.

Simon

[wkahl]

This should have been 7.0.1 - I'll try to reproduce this after Feb. 21.

[igloo]

Please reopen if you have a way to reproduce this.