问题标签 [proof-general]

我正在尝试将 coq 与 ProofGeneral 一起使用，但内置的 Verilog 模式会影响*.v文件类型识别。我可以以某种方式禁用它并让 ProofGeneral 将它们重新映射到它的 coq 模式吗？

这个问题与在 Emacs 中的 Proof General 中配置 Coq 模式有关。

我试图让 Emacs 用相应的 Unicode 字形自动替换 Coq 中的关键字和符号。我设法将其定义fun为希腊小写 lambda λ、forall通用量词符号 ∀ 等。我在定义单词符号时没有遇到任何问题。

问题是当我尝试为它们的 Unicode 符号 ⇒→↔ 定义运算符=>时->，<->它们不会被 Coq 中相应的 Unicode 字形替换。*scratch*但是，当我测试它们时，它们会在缓冲区中被替换。我使用相同的机制将 Unicode glyps 与 Coq 表示法匹配：

我怀疑问题在于 Coq 模式将某些标点符号标记为特殊，因此 Emacs 忽略了我的代码以将它们替换为 Unicode 字形，但我不确定。有人可以为我解释一下吗？

编辑 4：事实证明，这实际上只是一般 TTY 输入的限制；导致问题的 OCaml、Coq 或 Emacs 没有任何具体内容。

我正在使用 Emacs 中的 Proof General 开发 Coq 程序，但我发现了一个输入太长的错误。如果要通过 Proof General 提交的区域coqtop包含超过 1023 个字符，Proof General（虽然不是 Emacs）在等待响应时会挂起，并且*coq*缓冲区包含一个额外^G字符，用于超过 1023 个字符。例如，如果一个 1025 个字符区域被发送到coqtop，那么*coq*缓冲区将以两个额外的字符结束^G^G。我无法继续文件中的这一点，我必须终止coqtop进程（使用终端C-c C-x或kill/killall从终端）。

关于这种限制的某些东西来自coqtop其本身。如果生成一个 1024 字符或更长的字符串并将其通过管道输入，例如通过运行

然后一切正常。（同样，coqc也可以正常工作。） 但是，如果我coqtop在终端中运行，我不能在一行上输入超过 1024 个字符，包括结束返回字符。因此，输入 1023 个字符的行然后按回车即可；但是在输入 1024 个字符后，按任何键，包括返回（但不包括删除等），只会发出哔哔声。事实证明ocaml（OCaml 顶层）具有相同的行为：

ocaml工作正常，但如果从终端运行，我不能在一行上输入超过 1024 个字符。由于我的理解是coqtop依赖于 OCaml 顶层（在运行时更明显coqtop -byte），我想这是一个相关的限制。

相关软件版本为：

• 来自Homebrew的OCaml 3.12.1 ；
• 来自Homebrew的Coq 8.3pl3（和 8.3pl2）；
• 证明总则4.1；
• 从Emacs 为 Mac OS X构建GNU Emacs 24.1.1 ；和
• Mac OS X 10.6.7。

我的问题是：

• 怎么样ocaml并且coqtop正在执行这个字符限制？为什么只用于来自终端或 Emacs 的输入，而不是来自管道或文件的输入？
• 为什么Proof General（明显）不知道这个限制会导致挂起错误和神秘^G的s？
• 我该如何解决这个限制？我的最终目标是在 Proof General/Emacs 中使用 Coq，因此可以避开潜在问题的解决方法。

编辑 3：在发现 Ocaml 顶层也存在 1024 个字符的输入限制（我想这是相关的）后，我添加了该信息并删除了原始问题描述，因为它已被完全掩盖和取代。（如有必要，请参阅编辑历史）。

我正在使用一些正则表达式，并且在查看我的一些匹配项时，我很好奇为什么 exec 函数会产生与它一样多的结果。

我只是想稍微澄清一下操作的内部工作原理，以便我对为什么正则表达式返回n 个结果感到更舒服，而不是仅仅接受它确实如此。

前任。

在上面的示例中，我明白了为什么它匹配“邮编或城市和州”，但我不知道为什么会产生第二个匹配未定义的值。

提前致谢。

当 Isabelle 在 ProofGeneral 中显示目标时，假设呈现为在它们周围有括号，如下所示：

然而，在 Isabelle/jEdit 中，这似乎已更改为元含义箭头：

虽然我知道前者有些不标准，但我发现它更容易阅读。有没有办法修改 Isabelle/jEdit 的行为，以旧的 ProofGeneral 样式打印出目标？

我在 Coq 中使用 ProofGeneral。当我执行 Cc C-return 时，Emacs 会突出显示 Coq 已处理的区域。这很好。但是，它会在下一行插入一个“=>”，这会覆盖输入的前两个字符。例如，目前我正在看

我怎样才能摆脱那个箭头？

更新：

我了解到，如果我打开边缘模式，箭头就在边缘，我可以看到我所有的打字。不过我还是想杀了它。谢谢！

我在 Aquamacs 上的 Emacs 中使用 Proof General 并且每次我写一个句点（“。”）时，一切都会被执行（直到那个句点）。这似乎是一种电动行为，但事实并非如此。所有其他键的行为正常。

我知道这是我不小心使用了一些键绑定时开始的某种模式。如果我重新启动会话，效果将停止，但我想知道使其停止（或启动）的键绑定。

你知道这种模式叫什么吗？我什至在网上都找不到。

我是Isabelle和Proof General的新手。

我正在尝试在 Proof General 中设置一个深色主题以与 Isabelle 一起使用，但无论我选择什么主题（例如tango-dark、ample、monokai等），未触及的内部语法都会以非常难以阅读的绿色突出显示。我研究了自定义主题，但还没有弄清楚在哪里自定义它。下面是中的截图tango-dark。

是否存在与 Isabelle 配合得很好的漂亮深色主题，或者我如何在 Proof General 中自定义 Isabelle 内部语法的突出显示？

我只在运行 Proof General 时遇到这个问题。我假设这是由 Proof General 启动的一些随机次要模式，但无法确定是哪一个！我在下面列出了一些次要模式，以防你能认出这个名字。

如果我在 Emacs 中放置一个句点，光标会在它之前跳转，如下所示：

写东西|

写东西。|

写东西|。

where|代表光标，最后两行紧接着发生。

如果我单击带有句点的行尾，也会发生同样的情况。光标将出现在句号之后并立即跳转到句号之前。

某句。（点击这里）

某句。|

某句|。

最后两条线一个接一个地立即发生。

以下是次要模式的列表，以防您发现名称：

在大多数 IDE 或文本编辑器中，您可以右键单击一个术语，然后它会将您带到定义该术语的文件。CoqIDE 似乎没有，所以我一直在做coqdoc myfile.v --html，然后转到生成的 HTML 文档。但该文件中唯一可点击的术语是针对 Coq 标准库的。ssreflect 定义的术语（例如）不可点击。

在 Coq 文件中，是否有一种标准方法可以快速查找定义某些术语/标识符的位置（及其源代码）？在 CoqIDE 或 emacs + ProofGeneral 中（我正在使用 CoqIDE，但如果 emacs/ProofGeneral 有这种能力，我会切换）。

还是为您使用的每个 Coq 项目和依赖项生成文档的标准方法？