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

我在Isabelle（即最新版本Isabelle2013-2）中遇到性能问题。我使用Isabelle/JEdit，基于新界面。Isabelle：版本的性能问题Isabelle2013-2

所以之前的情况是我的表现有些麻烦。但现在情况变得更糟了，因为有时我需要等10秒才能进入正确的状态。随着时间的推移，性能问题会变得更糟，因为我必须在一小时左右后重新启动Isabelle。

我怀疑是我可以更好地配置Isabelle或应用一些提高性能的技巧。

硬件：最近
CPU，它是英特尔酷睿i7四核（移动的labtop芯片），16GB内存，快速的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的右下角仅显示约900mb。我有16GB内存，我应该配置Java使用更多的内存？有时单个进程会消耗600％的CPU，即Linux内核看到的6个内核。

技巧我用：

一个诀窍是，我在我的工作下面的代码行插入*)。这会导致语法错误，并且不检查下面的代码。第二个诀窍是我去了时间控制面板，所有花费超过0.2秒的证明我都注释掉了，换成sorry。

最新的两个伊莎贝尔版本是非常大的改进！

任何建议或窍门，我可以如何提高伊莎贝尔的表现？

来源

2014-01-12 mrsteve

请评论，如果我需要澄清我的表现问题或需要提供详细信息。 – mrsteve

你为什么要关闭这个？性能技巧可能对未来的伊莎贝尔版本也有效。 – mrsteve

PIDE的Perf问题将持续多年;他们更多是一个错误类型的报告。从表面看，只有一个人单独开发了Iszel/jEdit，这是Wenzel。他似乎也在追踪其他开发者报告的涉及Isa/jEdit的问题，这些问题不一定是他的错。他通常会在错误类型报告的邮件列表上做出回应。在isa邮件列表中，我认为Isa2013-2并不完全正确。我已经报道了几件可以完全挂住PIDE的东西，但这是进步的一部分。我把坏与好。 – 2014-01-12 17:44:26

数只表现调谐一般提示：

人们需要区分伊莎贝尔/ ML（即底层多晶硅/ ML运行时）对伊莎贝尔/ Scala中（即底层JVM）。 Isabelle/ML：像i7这样的Intel CPU具有超线程技术，这实际上使内核数量翻了一番。在较小的移动机器上，通常将核心的标称数量限制为一半的更好。请参阅Isabelle/jEdit/Plugin选项/ Isabelle/General中的“threads”选项。当使用电池运行时，您甚至可以在更低的地方进行。
Isabelle/ML：使用x86（32位）Poly/ML通常会提高性能。这只与Linux相关，因为该平台通常缺乏其他平台常规提供的x86库。回到笨重的x86_64几乎没有任何好处。 Poly/ML 5.5.x非常适合在32位模式的恒定空间中工作。 Isabelle/Scala：通过使用本机x86_64（这是默认设置）并提供大量的堆栈和堆参数，可以提高JVM的性能。
- 主要伊莎贝尔应用程序包的自举JVM一些选项是硬连线在某个地方，其仍然可以被编辑：
  - Linux操作系统：Isabelle2013-2/Isabelle2013-2。运行
  - 的Windows：Isabelle2013-2/Isabelle2013-2.ini
  - 的Mac OS X：Isabelle2013-2.app/Contents/Info.plist
  例如，最大堆大小可以从-Xmx1024m更改为-Xmx4096m。
- isabelle jedit命令行工具是通过Isabelle设置环境配置的。有关JEDIT_JAVA_OPTIONS的一些示例，请参阅$ISABELLE_HOME/src/Tools/etc/settings，该示例可以复制到$ISABELLE_HOME_USER/etc/settings并相应地进行修改。也可以通过jconsole来监控JVM的性能，以了解这实际上是否是问题的根源。
伊莎贝尔/斯卡拉：伊莎贝尔束一定JVM，其在此假定由默认。 Java版本的这种变量消除对于重新获得一些理智很重要 - 否则你永远不知道你得到了什么。你确定你的OpenJDK实际上在这里使用吗？这是不可能的，除非你编辑了一些伊莎贝尔设置。

Linux上性能问题的其他来源是图形。 Java/AWT在X11上比在Windows和Mac OS X上慢得多。在Linux上使用准本地GTK外观会进一步降低图形性能。

来源

2014-01-13 18:10:43 Makarius

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

回答

相关问题