我有一个by eval有点慢的证明，我想优化代码。by eval为了不那么盲目地这样做，如果 jEdit 可以显示进行证明所花费的时间，那就太好了。
Isabelle 2013 有可能吗？
问问题
173 次
1 回答
2
Isabelle 可以像 Perl 一样，有不止一种方法可以做到这一点。
在看到Isabelle 用户列表上的一些建议后，在 jEdit 中，我打开和关闭计时信息的方式与打开show_types和关闭命令之类的方式相同。
我导入一个文件，i.thy如下所示：
theory MFZ
imports Complex_Main "../../../../../../ithy/i"
begin
要查看时序信息，在 中i.thy，我有一堆信息命令，一个是命令
ML_command "Toplevel.timing := false"
我在 中将其设置为 true i.thy，在我的工作中我开始将by语句更改为apply，然后by在我在输出面板中看到时间信息后返回。
要关闭计时信息，您必须将true背面更改为false. 你不能只删除ML_command "Toplevel.timing := true".
如果您有一系列apply语句作为证明，您可以将时间总结相加，或者将它们组合在一个apply/by语句中，以获得单个apply语句的时间，例如切换语句
apply(simp)
apply(rule)
by(auto)
至
apply(simp,rule,auto)
编辑命令并更改false为true，或反之亦然，可能并不比涉水通过菜单完成相同的事情慢多少。
您可以创建一个 jEdit 宏以将命令插入您正在工作的位置，但是您必须突出显示它并在不再需要它之后将其删除。
这是我如何保持两个视图打开的图像。右视图显示我设置Toplevel.timing为 true 的位置，左窗口显示我将 a 更改by为 的位置apply。图像大小为 1211x488 ，在我的Chrome 中看起来不错。
http://gc44.github.io/viz/img_1300/130502a__toplevel_timing.png
于 2013-05-02T11:58:11.487 回答