segfault in Data.HashTable, triggered by long Agda runs
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
Trac metadata
Trac field | Value |
---|---|
Version | 7.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | libraries/base |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |