如何在 Isabelle/jEdit 中启用“跟踪”答案

【问题标题】：How to enable "Tracing" in Isabelle/jEdit如何在 Isabelle/jEdit 中启用“跟踪”
【发布时间】：2013-09-26 01:47:39
【问题描述】：

我是 vim 的粉丝，但只有 emacs 有这个 Isabelle/HOL 环境。 jEdit 很好，但是我不能用

using [[simp_trace=true]]

类似于 emacs。

如何在jEdit中启用“跟踪”？

【问题讨论】：

你是指追踪简化器，还是其他追踪？
您使用的是 Isabelle2013 版本附带的官方 Isabelle/jEdit 吗？
顺便说一句：除了 Isabelle，我也在使用 vim，曾几何时，我觉得我必须从 vim 内部使用 Isabelle（特别是因为唯一的选择是 emacs）。当时我的一个学生实现了一个允许与 Isabelle 交互的 vim 插件（长期弃用）。但这远不如 Proof General 并且永远不会像通过 Isabelle/jEdit 底层的文档模型与 Isabelle 交互一样流畅。所以我早就放弃了这种冲动；）
克里斯是对的。您不应该将 Isabelle/jEdit 放入纯文本编辑器的类别中。这就是我们将其定位为“Prover IDE”的原因。

标签： isabelle

【解决方案1】：

您确实可以在 Isabelle/jEdit 的证明中间使用 simp_trace，如下所示：

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

或者，您可以全局声明它，如下所示：

declare [[simp_trace]]

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

当您的光标位于 jEdit 中的 apply simp 语句之后时，两者都会在“输出”窗口中为您提供简化器的跟踪。

【讨论】：

【解决方案2】：

如果您需要深度大于 1（默认）的跟踪深度，您可以通过

对其进行微调

declare [[simp_trace_depth_limit=4]]

这个例子给出的跟踪深度为 4。

【讨论】：

【解决方案3】：

正如其他人指出的那样，您可以使用 simp_trace。但是，您也可以将 simp_trace_new 与“Simplifier Trace”窗口结合使用。这提供了优于 simp_trace 的改进输出：

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

要查看跟踪，请将光标放在“应用（自动）”上，然后单击“查看简化跟踪”。 “简化器跟踪”窗口（选项卡）应该打开。单击“显示跟踪”，应出现一个新窗口，显示每个子目标的跟踪。

Isabelle/Isar reference 提供更多详情：

simp_trace_new 控制 Isabelle/PIDE 应用程序中的 Simplifier 跟踪，尤其是 Isabelle/jEdit。
这提供了简化器执行的重写步骤的分层表示。
用户可以通过指定断点、详细程度来配置行为并启用或禁用交互模式。
在正常冗长（默认）下，只有匹配断点的规则应用程序才会被显示给用户。在完全详细的情况下，将记录所有规则应用程序。交互模式会打断简化器的正常流程并推迟决定如何通过一些 GUI 对话框继续与用户联系。

您也可以指定“使用 [[simp_trace_new mode=full]]”link here 查看简化器采取的所有步骤。

注意：在前面的示例中，显示“apply(induction xs)”的跟踪不会产生任何输出。

【讨论】：