id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
4805	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"	bug	closed	normal	7.2.1	libraries/base	7.0.1	invalid	Data.HashTable segfault	hackage.haskell.org@…	Linux	x86_64 (amd64)	Runtime crash