I have adopted our sources now so that they also work with fgl-5.4.1. So neither ghc-6.6.1 nor fgl-5.4.1 need to change. The problem was that "inn" returns loops since fgl-5.4, that led to more edges to be processed (by our function selectProofBasis). Another problem (not relevant for our performance loss, though) is that "inn" and "out" both return the same loops, which may lead to a duplication of loops if reinserted. Further technical comments below. Christian Christian Maeder schrieb:

I wrote:

...

Dear Hets- and GHC-Developers,

...

we have a problem using ghc-6.6.1. The created hets binary runs a couple of times slower than the one created using ghc-6.6.

This problem is gone when I install and use fgl-5.3 (where "hiding (indices)" needs to be deleted in Data.Graph.Inductive.Monad.IOArray).

I strongly suspect the new functions context1l' and context4l' in Data.Graph.Inductive.Graph (fgl-5.4.1) to be the reason for our drastic slow down.

In fgl-5.3 the functions fst4 and fth4 have been used instead. A cyclic edge (an edge from and to the very same node) was only returned as ingoing edge and not as outgoing one. (a design decision documented elsewhere).

I think, the change in fgl-5.4.1 now returns a cyclic edge also as outgoing edge (and possibly twice as ingoing one).

Exchange in- and outgoing (and cyclic edge with loop). The loops are not duplicated by a single call. Just the function matchGr (method match) from Data.Graph.Inductive.Tree returns the loops as successors only. (Therefore the filtering in context4l' might be just unnecessary for this instance) context1l' :: Context a b -> Adj b context1l' (p,v,_,s) = p++filter ((==v).snd) s context4l' :: Context a b -> Adj b context4l' (p,v,_,s) = s++filter ((==v).snd) p