如何从命令行验证* .thy文件是有效的Isabelle证明？我猜想在GUI中执行此操作等于看到没有问题/错误/警告等。但是有没有办法从命令行执行此操作？
最佳答案
您只需要编写一个小的ROOT文件，然后调用isabelle build即可。
例如，如果要检查Foo.thy和Bar.thy理论是否已编译，则可以创建一个名称为ROOT的文件，其内容如下:
session Test = HOL +
theories
Foo
Bar
然后可以通过编译完成
isabelle build -d. Test
有关更多详细信息，请参见《 Isabelle系统手册》(第2章)。
关于command-line - 从命令行验证Isabelle证明，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/48939929/