Isabelle2016 和命令行
Isabelle2016 and command line
我是 Isabelle 的新手，现在正在尝试使用 Cygwin 的命令行进行证明，以测量证明引理所需的时间。
最好和最简单的方法是什么？
我希望有一个像这样的命令："isabelle theory_file.thy"，但是通过伊莎贝尔系统手册 运行 我觉得一切都比这复杂得多，最终迷路了。
所以我有一个理论文件，正在寻找一种方法来使用包含在 Isabelle2016 发行版中的 Cygwin 终端开始证明过程 Windows。
非常感谢我需要参考的每条建议或方向。
提前致谢。
如果你只是使用普通的Prove IDE (Isabelle/jEdit)，你可以得到各个命令的时序信息如下：
CONTROL-将鼠标悬停在命令关键字上：显示花费可测量时间（超过 1 毫秒）的命令的计时。
Isabelle/jEdit 菜单项 "Plugins / Isabelle / Timing" 为理论和命令提供了单独的计时面板，另请参阅标签为 jedit[=27 的 Isabelle 文档=].
如果您真的需要 while 会话的批处理模式计时（其中包含所有理论），最简单的方法是通过 isabelle build -v。请参阅 system 手册（在 "Isabelle sessions and build management" 部分）。
请注意，默认情况下一切都并行运行，因此计时结果始终需要合理的解释。
我是 Isabelle 的新手，现在正在尝试使用 Cygwin 的命令行进行证明，以测量证明引理所需的时间。
最好和最简单的方法是什么？
我希望有一个像这样的命令："isabelle theory_file.thy"，但是通过伊莎贝尔系统手册 运行 我觉得一切都比这复杂得多，最终迷路了。
所以我有一个理论文件，正在寻找一种方法来使用包含在 Isabelle2016 发行版中的 Cygwin 终端开始证明过程 Windows。
非常感谢我需要参考的每条建议或方向。 提前致谢。
如果你只是使用普通的Prove IDE (Isabelle/jEdit)，你可以得到各个命令的时序信息如下：
CONTROL-将鼠标悬停在命令关键字上：显示花费可测量时间（超过 1 毫秒）的命令的计时。
Isabelle/jEdit 菜单项 "Plugins / Isabelle / Timing" 为理论和命令提供了单独的计时面板，另请参阅标签为 jedit[=27 的 Isabelle 文档=].
如果您真的需要 while 会话的批处理模式计时（其中包含所有理论），最简单的方法是通过 isabelle build -v。请参阅 system 手册（在 "Isabelle sessions and build management" 部分）。
请注意，默认情况下一切都并行运行，因此计时结果始终需要合理的解释。