The proved implementation of the priority queue is slow

[dinosaure]

Currently, from some benchmarks, it seems that the huge bottleneck is Pqueue.extract_min_exn (which re-balances the priority queue). The Domain_elt.compare is also called a lot (probably due to cancelled tasks). We should take a deeper look on the implementation.

[dinosaure]

I've noticed quite a few allocations in the major heap with this implementation but with other observation tools, it seems that Miou_pqueue (the proved impl.) isn't Miou's biggest problem. There are still some interesting areas for optimisation (inlining of Vector.get, the functor doesn't allow you to inline the function compare elements, etc.). It's clearly a low priority.

I'll leave this issue open, however, if one day implementation becomes a real problem.