Isabelle: Isabelle2013-2版本的性能问题

Question

我在Isabelle中有性能问题(也就是最新版本Isabelle2013-2)。我使用基于新接口的Isabelle/JEdit，。

所以之前的情况是我在表演上遇到了一些麻烦。但现在情况更糟了，因为我有时要等10秒才能进入右边。随着时间的推移，性能问题变得越来越糟糕，关键是我不得不在一小时左右后重新启动伊莎贝尔。

我怀疑我可以更好地配置Isabelle，或者使用一些技巧来提高性能。

硬件：

最近的CPU，它是一个英特尔i7四核(移动实验室芯片)，16 it内存，快速的SSD硬盘。

软件：

64位arch linux (内核3.12.5-1-ARCH)

没有32位兼容性库

我的java版本是：

   java version "1.7.0_45"
   OpenJDK Runtime Environment (IcedTea 2.4.3) (ArchLinux build 7.u45_2.4.3-1-x86_64)

我的理论文件有125KB大小，我正在工作的全部理论都在一个文件中，但现在我真的很想要一个文件。

症状：伊莎贝尔在UI的右下角只显示大约900 UI。我有16 to的RAM，我应该配置java来使用更多的RAM吗？有时，单个进程消耗了600%的CPU，即linux内核看到的6个内核。

我使用的技巧：

其中一个技巧是，我将*)插入到我正在处理的代码下面的一行。这将导致语法错误，下面的代码将不被检查。第二个窍门是，我去了计时面板，所有的证明都花了超过0.2秒的时间，我把它注释掉，换成了sorry。

最近的两个伊莎贝尔版本真的是很大的改进！

对我如何提高伊莎贝尔的表现有什么建议或窍门吗？

Answer 1

关于性能调优的一些一般性提示：

• 我们需要区分Isabelle/ML (即底层Poly运行时)和Isabelle/Scala (即底层JVM)。
• 伊莎贝尔/ML:像i7这样的英特尔CPU有超线程，这几乎是内核数量的两倍。在小型移动机器上，通常最好将核的名义数量限制在其中的一半。请参阅Isabelle/jEdit / Plugin Options / Isabelle / General中的“线程”选项。当你在电池上运行时，你甚至可能会走得更远。
• 伊莎贝尔/ML:使用x86 (32位)Poly通常可以提高性能。这仅与Linux相关，因为该平台通常缺乏其他平台常规提供的x86库。很少有任何好处回到笨重的x86_64。PolyML5.5.x在32位模式的恒定空间中工作能力很强。
• Isabelle/Scala:通过使用本机x86_64 (这是默认的)并提供慷慨的堆栈和堆参数，可以提高JVM的性能。

- The main Isabelle application bundle bootstraps the JVM with some options that are hard-wired in a certain place, which can be edited nonetheless:

    - Linux: Isabelle2013-2/Isabelle2013-2.run
    - Windows: Isabelle2013-2/Isabelle2013-2.ini
    - Mac OS X: Isabelle2013-2.app/Contents/Info.plist

例如，最大堆大小可以从-Xmx1024m更改为-Xmx4096m。

- The `isabelle jedit` command-line tool is configured via the Isabelle settings environment.  See also `$ISABELLE_HOME/src/Tools/etc/settings` for some examples of `JEDIT_JAVA_OPTIONS`, which can be copied to `$ISABELLE_HOME_USER/etc/settings` and adapted accordingly.  It is also possible to monitor JVM performance via `jconsole` to get an idea if that is actually a source of problems.

​

• Isabelle/Scala: Isabelle捆绑了一个特定的JVM，默认情况下在这里假设。这个Java版本的变量消除对于恢复一些理智是很重要的，否则你永远不知道你得到了什么。你确定你的OpenJDK真的在这里被使用了吗？这是不可能的，除非你已经编辑了一些伊莎贝尔设置。

Linux上性能问题的进一步来源是图形。众所周知，X11上的Java/AWT要比在Windows和Mac上慢得多。在Linux上使用准原生的GTK外观会进一步降低图形性能。