The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

Coq has at least one big memory leak.   Currently we're working on one such case in https://github.com/coq/coq/issues/12487.

Jim

On Wed, Jun 17, 2020 at 11:00 AM Samuel Gruetter <gruetter AT mit.edu> wrote:

I think the problem is that if you want to define an eq_dec for a type with n
constructors, you need a term of size n^2, so here's a way to get similar
definitions (not sure if similar enough for what you need) without requiring
one big Inductive for "constructor":

Definition decidable (P: Prop) := {P} + {~P}.
Definition eq_dec T := forall (x y:T), decidable (x=y).

Inductive spec_type: Set :=
| abruption
... same as before
.

Inductive constructor_of_abruption: Set :=
| AnomalyAbruption : constructor_of_abruption
| NotImplemented : constructor_of_abruption
| ObjectAbruption : constructor_of_abruption.

... one separate Inductive per spec type

Definition constructor(t: spec_type): Set :=
  match t with
  | abruption => constructor_of_abruption
  | ... => ... 157 more cases, but not inside an Inductive!
  end.

Scheme Equality for constructor_of_abruption.
... 157 more of them

Definition constructor_eq_dec(t: spec_type): eq_dec (constructor t) :=
  match t with
  | abruption => constructor_of_abruption_eq_dec
  | ... => ...
  end.

The full file is here:
https://gist.github.com/samuelgruetter/01db98f43a8dc57f7d70f7d12e48eb20
(I couldn't attach it to the email because apparently the maximum message
size on this list is 39 kB).

On my machine, "/usr/bin/time -v coqc js.v" says it runs within 1GB of RAM
and 17s, which I'd consider ok. And most of the time (~15s) is spent in on
one single line:

Time Scheme Equality for constructor_of_intrinsicObject.

because that one has 110 constructors.

On Wed, 2020-06-17 at 15:44 +0200, Alan Schmitt wrote:
> Hello,
>
> As part of a larger project, I'm generating a big inductive type for
> which I need to prove decidable equality. Running ~coqc js.v~ on the
> attached file result in a Stack Overflow. I tried duplicating the line
> where the problem occurs (instead of using "all:"), but I then run out
> of memory and coqc is killed.
>
> I feel like I'm not using the correct approach. Do you have suggestions
> on how to deal with this?
>
> Thanks,
>
> Alan
>