Иногда появляется лемма, где try0 падает Изабель/JEdit. Тогда работает только kill -9 на идентификаторе процесса.Isabelle: запустить команду try без try0
Когда я тогда звоню try в такой же ситуации, Isabelle/JEdit снова сработает.
Можно ли в этой ситуации вызывать все от try без пробега try0 (или иначе опустить все доказательства try0)?
(. Я сделал некоторые поиски Google, но не смогли найти что-либо отношение)
С isar-ref.pdf, стр 267, это дает следующие указания на try0 и try:
solve_direct, quickcheck, try0, sledgehammer, nitpick).Так что, если описание завершено в справочном руководстве Изар, то try является try0 плюс два пруверы, solve_direct и sledgehammer и два контрпример искатели, quickcheck и nitpick.
Чтобы не запускать датчики try0, насколько мне известно, вам нужно было бы запустить solve_direct и sledgehammer отдельно.
Если try0 висит на PIDE, то это в основном, вероятно, происходит в плохую петлю какого-то, где позволяя Auto Methods в Plugin Options/Isabelle может также вызвать эту петлю, так как он делает что-то похожее на try0.
Есть два вида петель, которые я испытал, когда я могу вспомнить только 2-ую в списке рядом, как подвешивания PIDE:
simp правила петли, вызванные simp или методы, которые требуют simp, таких as auto, force, fastforce, slowsimp, и bestsimp. Чтобы остановить бесконечный цикл, мне просто нужно удалить команду.blast Петли, вызванные auto, вызывающие blast. Для такого рода это происходит либо сразу, либо после того, как я разрешаю команде работать в течение 5 секунд или около того.Вы можете попытаться сузить который автоматический метод доказательства вызывает try0 и try повесить PIDE.
Вы можете получить список try0 используемых методов, как это (я не знаю, если список испытателей он показывает полный):
lemma "False"
try0
(*Trying "simp", "auto", "fast", "fastforce", "force", "blast", "metis",
"linarith", and "presburger"...*)
oops
Из этого списка, если apply(simp) зацикливается, вы знаете, что существует цикл правил simp (или правила simp, которые занимают много времени), что сделало бы auto, fastforce и force loop, так как они звонят simp.
Если auto зацикливается, то это может быть simpblast или, так auto может позвонить каждый из них, так что вы можете попробовать apply(blast), чтобы увидеть, если blast проблема.
С Isabelle2013-2 для меня висит PIDE из-за auto, потому что он вызывает blast. Предположительно, это было исправлено для следующего выпуска.
Я поставил это как второй ответ, так как он достаточно разный.
Я просматривал изменения в хранилище, и это привело меня к следующим файлам Isabelle2013-2 ML, связанным с try и try0 (но не заперт в полностью, потому что список других файлов, чтобы показать все меняется) :
Файл try.ML дает эту строку источника:
val get_tools : theory -> tool list
Я полагаю, используя ML, человек может получить список инструментов, используемых try, но если это так, то это, вероятно, соответствует описанию, приведенному в другой ответ от isar-ref.pdf.
В принципе, есть try, который вызывает другие инструменты, sledgehammer, который делает свою особую вещь, где использование try0 является частью арсенала, solve_direct, а затем полностью автоматические методы доказательства, используемые try0, которые перечислены в try0.ML ,
Большинство автоматических методов доказательства, которые перечислены в try0.ML упоминаются в isar-ref.pdf разделах
Теперь некоторые изменения, которые идут вниз по трубе, взят из последних файлов или ревизий:
Из последнего репозитория try0.ML он дает список методов доказательства th на try0 попробует. Если вы посмотрите на Isabelle2013-2 try0.ML выше, вы увидите, что список, указанный в этом файле, представляет собой тот же список методов, показанных в другом ответе при попытке доказать False.
Здесь есть дополнительные автоматические методы доказательства, которые в настоящее время не используются с Isabelle2013-2.
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest");
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest");
val simp_attrs = (SOME "add", NONE, NONE, NONE);
val metis_attrs = (SOME "", SOME "", SOME "", SOME "");
val no_attrs = (NONE, NONE, NONE, NONE);
(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
val named_methods =
[("simp", ((false, true), simp_attrs)),
("auto", ((true, true), full_attrs)),
("blast", ((false, true), clas_attrs)),
("metis", ((false, true), metis_attrs)),
("linarith", ((false, true), no_attrs)),
("presburger", ((false, true), no_attrs)),
("algebra", ((false, true), no_attrs)),
("fast", ((false, false), clas_attrs)),
("fastforce", ((false, false), full_attrs)),
("force", ((false, false), full_attrs)),
("meson", ((false, false), metis_attrs))]