3

Isabelle has a quick_and_dirty mode that allows proofs to be skipped with sorry. It is enabled by default in jEdit and disabled by default with isabelle build. How can I change the setting

  • In jEdit (interactively or with a command line parameter),
  • For isabelle build, from the command line,
  • For isabelle build, in the ROOT file, respectively.

Also, are there other means of asking Isabelle, preferably interactively in jEdit, “What lemmas in the current theory and its parents have been proven using a sorry“?

(I am asking this here in the hope that there will always be up-to-date-answers, in contrast to some mailing list posts that I find with google.)

4

1 回答 1

2

我不知道有什么方法可以实现您的第一点（对于 jEdit），对于其他点应该是

isabelle build -o quick_and_dirty ...
isabelle build -o quick_and_dirty=true ... # same as the previous command
isabelle build -o quick_and_dirty=false ...

和

session Foo = HOL +
  options [quick_and_dirty] (*with the same variants as above*)
  theories A B

（在您的ROOT文件中），分别。或者对于个别理论，例如，

session Foo = HOL +
  theories [quick_and_dirty] A
  theories B

另请注意，命令行选项会覆盖文件中设置的选项ROOT。

于 2013-09-05T08:43:44.233 回答