Isabelle2016和命令行

Question

我是伊莎贝尔的新手，现在我试着用Cygwin的命令行来证明一个引理所需的时间。

做这件事最好和最简单的方法是什么？

我预计会有这样的命令："isabelle theory_file.thy"，但是在运行了Isabelle系统手册之后，我觉得一切都比这个复杂得多，最终就迷路了。

因此，我有一个理论文件，并正在寻找一种方式，开始一个证明进程，包括Cygwin终端包括在Isabelle2016发行版的Windows。

我需要寻求的每一条建议或方向都受到高度赞赏。提前谢谢。

Answer 1

如果您只使用普通的凭证IDE (Isabelle/jEdit)，您可以获得各个命令的定时信息，如下所示：

• 控制-悬停在命令关键字上:对花费可测量时间(超过1毫秒)的命令显示定时。
• Isabelle/jEdit菜单项"Plugins / Isabelle / Timing“为理论和命令提供了一个单独的计时面板，请参见带有标签jedit的伊莎贝尔文档。

如果您确实需要批处理模式的同时会话(其中的所有理论)，最简单的方法是通过isabelle build -v。请参阅system手册(在"Isabelle会话和构建管理“一节)。

注意，默认情况下，所有事情都是并行运行的，所以计时结果总是需要合理的解释。