coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s)

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s)
Date: Mon, 2 Feb 2015 08:29:04 +0000
Accept-language: de-DE, en-US

Dear Coq Users,

one thing which doesn't look right in CoqIDE 8.5 (Windows) is that the
checking of trivial proofs with the asynchronous proof mechanism is very
slow. As it looks any proof takes at least 15s. So a simple file with 4
trivial proofs takes more than 1 minute, although coqc can check it in a
fraction of a second.

Best regards,

Michael

[Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s), Soegtrop, Michael, 02/02/2015
- Re: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s), Enrico Tassi, 02/02/2015
  - RE: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s), Soegtrop, Michael, 02/02/2015
    - Re: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s), Enrico Tassi, 02/02/2015
  - Re: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow (always >15s), Pierre-Marie Pédrot, 02/02/2015