coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Memory consumption issue with Containers.Maps

From: Justus Matthiesen <justus.matthiesen AT cl.cam.ac.uk>
To: coq-club AT inria.fr
Cc: stephane.lescuyer AT inria.fr
Subject: [Coq-Club] Memory consumption issue with Containers.Maps
Date: Tue, 27 Nov 2012 16:29:38 +0000

I've been trying to use Lescuyer's Containers library for Coq 8.4 [1].

When feeding

Require Import Containers.Sets.
Check set.

to coqtop, it dutifully reports

set : forall (A : Type) (H : OrderedType A), FSet -> Type

In contrast, when given

Require Import Containers.Maps.
Check map.

coqtop starts eating all the memory available. Is it a known bug?

Thanks,
Justus

[1] http://coq.inria.fr/pylons/contribs/files/Containers/v8.4

[Coq-Club] Memory consumption issue with Containers.Maps, Justus Matthiesen, 11/27/2012
- Re: [Coq-Club] Memory consumption issue with Containers.Maps, David Pereira, 11/27/2012
  - Re: [Coq-Club] Memory consumption issue with Containers.Maps, Justus Matthiesen, 11/27/2012
    - Re: [Coq-Club] Memory consumption issue with Containers.Maps, David Pereira, 11/28/2012
      - Re: [Coq-Club] Memory consumption issue with Containers.Maps, Arnaud Spiwack, 11/29/2012