Как включить трассировку в Isabelle / jEdit

Я фанат vim, но только emacs имеет эту среду Isabelle / HOL. jEdit великолепен, но я не могу использовать

using [[simp_trace=true]]

как в emacs.

Как включить «Трассировку» в jEdit?


isabelle
person njuguoyi    schedule 26.09.2013    source источник
comment
Вы просто имеете в виду отслеживание упрощителя или другое отслеживание?   -  person davidg    schedule 26.09.2013
comment
Вы используете официальный Isabelle / jEdit, который поставляется с выпуском Isabelle2013?   -  person chris    schedule 26.09.2013
comment
Кстати: для всего, кроме Изабель, я также использую vim, и однажды я почувствовал, что должен использовать Изабель изнутри vim (тем более, что единственной альтернативой был emacs). В то время мой студент реализовал плагин vim (давно устаревший), который позволял взаимодействовать с Изабель. Но это было намного хуже, чем Proof General, и никогда не было таким гладким, как взаимодействие с Изабель через модель документа, лежащую в основе Isabelle / jEdit. Так что я давно отказался от этого побуждения;)   -  person chris    schedule 26.09.2013
comment
Крис прав. Не следует помещать Isabelle / jEdit в категорию с текстовыми редакторами. Вот почему мы позиционируем его как Prover IDE.   -  person Makarius    schedule 09.10.2013

Ответы (3)


arrow_upward
11
arrow_downward

Вы действительно можете использовать simp_trace в середине доказательства в Isabelle / jEdit, например:

lemma "(2 :: nat) + 2 = 4"
  using [[simp_trace]]
  apply simp
  done

В качестве альтернативы вы можете объявить его глобально, например:

declare [[simp_trace]]

lemma "(2 :: nat) + 2 = 4"
  apply simp
  done

Оба дают вам трассировку упрощающего в окне «Вывод», когда ваш курсор находится сразу после оператора apply simp в jEdit.

person davidg    schedule 26.09.2013

arrow_upward
7
arrow_downward

Если вам нужна глубина трассировки более 1 (по умолчанию), вы можете настроить ее с помощью

declare [[simp_trace_depth_limit=4]]

В этом примере глубина трассировки равна 4.

person Holger B    schedule 26.02.2014

arrow_upward
3
arrow_downward

Как указывали другие, вы можете использовать simp_trace. Однако вы также можете использовать simp_trace_new в сочетании с окном «Simplifier Trace». Это обеспечивает улучшенный вывод по сравнению с simp_trace:

lemma "rev (rev xs) = xs"
  using [[simp_trace_new]]
  apply(induction xs)
  apply(auto)
  done

Чтобы просмотреть трассировку, наведите курсор на «применить (авто)», затем нажмите «Просмотреть трассировку упрощения». Должно открыться окно (вкладка) «Simplifier Trace». Нажмите «Показать трассировку», и должно появиться новое окно, показывающее трассировку для каждой подцели.

В справочнике Изабель / Изар содержатся дополнительные сведения:

simp_trace_new управляет трассировкой Simplifier в приложениях Isabelle / PIDE, особенно Isabelle / jEdit.
Это обеспечивает иерархическое представление шагов перезаписи, выполняемых Simplifier.
Пользователи могут настроить поведение, указав точки останова, многословность и включение или отключение интерактивного режима.
В обычном режиме подробности (по умолчанию ) пользователю будут показаны только приложения-правила, соответствующие точке останова. В полном объеме все приложения правил будут регистрироваться. Интерактивный режим прерывает нормальную работу Упростителя и откладывает решение, как продолжить, пользователю через какой-либо диалог графического интерфейса.

В качестве альтернативы вы можете указать "using [[simp_trace_new mode = full]]" ссылка здесь Чтобы увидеть все шаги, предпринятые упрощателем.

ПРИМЕЧАНИЕ: в предыдущем примере отображение трассировки «apply (индукция xs)» не дает выходных данных.

person Eduard Nicodei    schedule 25.12.2014