Как установить быстрый и грязный флаг в Isabelle

Question

Isabelle имеет режим quick_and_dirty, который позволяет пропускать доказательства с sorry. Он включен по умолчанию в jEdit и по умолчанию отключен isabelle build. Как я могу изменить настройки

• В jEdit (в интерактивном режиме или с помощью параметра командной строки),
• Для isabelle build, из командной строки,
• Для isabelle build, в файле ROOT соответственно.

Кроме того, есть другие средства просят Изабеллу, предпочтительно в интерактивном режиме в jEdit, «Что леммы в современной теории и ее родители были доказаны с помощью sorry«?

(Я спрашиваю об этом здесь, в надежде, что там всегда будет уточненный-ответы, в отличие от некоторых сообщений из списков рассылки, которые я нахожу с Google.)

Answer 1

Я не знаю ни путь к достижению вашей первой точки (для 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.