Isabelle2016和命令行

Question

我是Isabelle的新手，现在尝试使用Cygwin的命令行来测试证明引理所需的时间。

什么是最好和最简单的方法来做到这一点？

我希望有一个像“isabelle theory_file.thy”这样的命令，但已经通过了Isabelle系统手册。我有一种感觉，一切都比这更复杂，最终失去了。

所以我有一个理论文件，并正在寻找一种方法来启动一个证明过程，并将Cygwin终端包含在Windows的Isabelle2016发行版中。

我需要看的每一条建议或方向都非常感谢。 在此先感谢。

Answer 1

如果只是使用正常证明IDE（伊莎贝尔/ jEdit的），就可以得到用于各个命令的定时信息如下：

• CONTROL-悬停在命令关键字：定时显示用于命令该采取可测量的时间（超过1毫秒）。

• 的伊莎贝尔/ jEdit的菜单项“插件/伊莎贝尔/时序”提供了理论和命令的单独的定时面板，也看到了伊莎贝尔文档与标签jEdit的。

如果你确实需要的，而会话（其中的所有理论），最简单的方法是通过isabelle build -v批处理模式时序。请参阅系统手册（在“Isabelle会话和构建管理”一节中）。

请注意，默认情况下所有内容都是并行运行的，因此时间结果总是需要合理的解释。