The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

Could you try the same experiments with Coq 8.8? 8.3 is fairly old and
Coq's performance has improved in many areas since then.

If the numbers are still not good, I suggest you open an issue at
https://github.com/coq/coq/issues

Thank you!

Maxime.

On 05/08/2018 06:30 AM, Wilayat Khan wrote:
> Hello
> 
>   Am using tactic *destruct* over inductive variables of type bool with
> just two constructors. I observed, it takes too long (over 14 seconds)
> for the destruct to return when used for 14 variables at a time (e.g.,
> destruct a, b, c, d, e, f, g, h, i, j, k, l , m, n; simpl;auto) or used
> for individual variable, combined with ; (e.g., destruct a; destruct b;
> destruct c;...;simpl;auto). The time of execution increases with
> variables and terms.  Coq's performance is best at using destruct over 8
> variables at  a time. I am using Coq 8.3 on my 64bit Intel Core i5, 8GB
> RAM with 2.6GHz machine 
> 
> I am wondering, if there is any systemic study/analysis assessing the
> performance of Coq over *destruct* tactic (in particular case analysis
> on inductive type bool) and comparing Coq (or interactive theorem
> provers in general) with automatic solvers.  
> 
> Best, 
> 
> Wilayat
>