The Coq mailing list

[Jean Goubault-Larrecq <Jean.Goubault AT dyade.fr>]

Dear all,

        I've always thought that Compute and Eval Compute
implemented the same reduction strategy.  However,
in recent experiments I realized that Compute was between
3 and 4 times slower and used between 6 and 20 times more
space.  The even stranger thing is that Qed is faster than
Compute, although I am running all this on examples which
are meant to be fast under call-by-value.
        Is there any reasonable explanation?

        I am using Coq V6.3, and testing things like:
Coq < Time Eval Compute in (tauto (pb72 (5) (4))).
     = (ad_x xH)=(ad_x xH)
     : Prop
Finished transaction in 61 secs (53.01u,0.3s)

Coq < Fact gag : (tauto (pb72 (5) (4))).
Coq < Time Compute.
1 subgoal

  ============================
   (ad_x xH)=(ad_x xH)
Finished transaction in 260 secs (177.71u,2.1s)

gag < Time Reflexivity.
Subtree proved!
Finished transaction in 0 secs (0u,0.01s)

gag < Time Qed.
Compute.
Reflexivity.

gag is defined
Finished transaction in 146 secs (121.89u,0.6s)


        All the best,

        -- Jean.