coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] What can make CoqIDE slow?

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] What can make CoqIDE slow?
Date: Sun, 27 Mar 2011 22:18:18 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=V3ATT6LiFD0xEwhheRGK/qppLf5KtDmriPEzPI3/fUVM14L2Kc0EgnqsHOWIBZyDvd ZyqJ2BO3CV14hBqV9PvJDEhk7aeKO9c2A/v0D/8ngfK+LpcMCJ/8NRYxXN1bynm4LgNE rGx6Sc7HpZUKuOW0jjD3MXY0lqE8nC6LIZMP4=

Hi all,

I have CoqIDE 8.3 rc1 and 8.3 pl1. It is slow for some reason. During interactive proofs, I can observe that proof contexts at the top-right window are refreshed line-by-line. Generally proof contexts should be displayed in 0 sec w/o any delay. My proof is not complicated. It seems that CoqIDE takes a lot of computation on displaying proofs. And the proof is stuck or locked until the display is done. The 8.3 beta and the earlier 8.2 do not have the problem. Does anyone have the same experience? What can make CoqIDE slow?

Thanks.
--
Jianzhou

[Coq-Club] What can make CoqIDE slow?, Jianzhou Zhao