The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

1) Typeclass resolution may be a reason for long rewrite times. If so, the following may help

Typeclasses eauto := 5 (* or a small number, to limit the depth of search  *)

Typeclasses eauto := debug

For more, see the last section of https://coq.inria.fr/refman/Reference-Manual022.html#sec673

2) Most of MathClasses compiles on 8.5pl3. 

I have a branch where I fixed (for 8.5pl3 on Windows) the parts of MathClasses that I need  for my work.

https://github.com/aa755/math-classes/tree/Windows

Use the "-k" option of scons to compile as many Coq files as possible, and not give up on all files when 1 file fails to compile.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Nov 30, 2015 at 7:02 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

> On Nov 30, 2015, at 15:55 , Clément Pit--Claudel <clement.pit AT gmail.com> wrote:
>
> Could this be https://coq-bench.github.io/ (courtesy of Guillaume Claret)?

Yes thats the page. Thanks!

Unfortunately both CoLoR and math-classes are shown as “not compatible” with recent 8.5 betas so I am stuck with 8.4 for now and need to find a way to solve this problem under 8.4.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva