The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

Hi list,

We are observing a strange behavior of Eval (compute or lazy, doesn't
matter) in the ALEA library.

We are using Coq v8.2pl2. After declaring a few classes (not
implemented, just declared) there should be nothing to compute about
those classes, but Eval compute takes forever to realize this. Any
advice on what it could be doing, or how to find this out?

I only managed to minimize the issue to one file but it's still pretty
big, so I'll just share a summary. After a bunch of declarations, we
reach this point:

=====

Generalizable Variables D.

(** *** Definition of cpos *)
Class cpo  `{o:ord D} : Type := mk_cpo
  {D0 : D; lub: forall (f:nat -m> D), D;
   Dbot : forall x:D, D0 <= x;
   le_lub : forall (f : nat -m> D) (n:nat), f n <= lub f;
   lub_le : forall (f : nat -m> D) (x:D), (forall n, f n <= x) -> lub f <= x}.

Implicit Arguments cpo [[o]].

Module Type Universe.
Parameter U : Type.
Generalizable All Variables.
Declare Instance ordU: ord U.
Declare Instance cpoU: cpo U.

=====

Now the following returns immediately as expected:
  Eval compute in (let (_,_,_) := ordU in True).

But this one takes forever:
  Eval compute in (let (_,_,_,_,_) := cpoU in True).

Cheers,

David