7

编辑 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 字符或更长的字符串并将其通过管道输入，例如通过运行

perl -e 'print ("Eval simpl in " . (" " x 1024) . "1.\n")' | coqtop

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

perl -e 'print ((" " x 1024) . "1;;")' | ocaml

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

相关软件版本为：

我的问题是：

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

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

4

2 回答 2

5

我在 OCaml 错误跟踪器上将此报告为问题 5678，用户 dim 解释说这不是 OCaml本身的问题，而是 TTY 输入的限制。问题是这样的。由于在用户点击返回之前文本不会发送到正在运行的命令，因此所有等待的输入都必须存储在某个地方。存储它的缓冲区，称为输入队列或预输入缓冲区，具有固定大小，由 C 常量控制MAX_INPUT。 这个常数在 Mac OS X 上等于 1024。像这样的缓冲允许对输入进行有用的处理，例如在发送字符之前删除字符。从终端运行的所有不做特殊事情（例如使用readline库）的命令都会表现出这种行为；例如，cat chokes in exactly the same way.

To avoid this behavior, one can unset the ICANON flag, for instance by running stty -icanon; this puts the TTY into non-canonical input mode, where input is not processed at all before being sent to the command. This means that editing becomes impossible: delete, left and right arrows, and so on all enter their literal equivalents (^?, ^[[D, ^[[C, …); similarly, ⌃D no longer sends an EOF, but merely a literal control character. However, for my particular use case, this (so far!) seems to be ideal, since Emacs is handling all my input for me. (Edit: But there's a better option!) (Libraries like readline，据我了解，也更改此设置，但要注意控制字符和处理编辑等。）要恢复规范模式，可以运行stty icanon.

该ledit工具将行编辑包装在作为参数提供给它的程序周围，因此ledit coqtop可以正常工作（如果奇怪的话；我更喜欢ledit -l 65536避免它的滚动），但与 Emacs 的交互却很奇怪。该rlwrap工具做同样的事情，但让其他程序从 TTY 读取；因此，虽然它可以接收更长的输入，但按 enter 并将它们发送到包装的命令会表现得非常奇怪，最终需要终止该命令。

Edit: In my specific use-case, I can also simply tell Emacs to use a pipe instead of a PTY, solving the problems at a stroke. The Emacs variable process-connection-type controls how subsidiary processes are communicated with; nil means to use a pipe, and non-nil means to use a TTY. Proof General uses the variable proof-shell-process-connection-type to determine how this should be set. Using a pipe solves all the 1024-character-limit problems.

于 2012-07-11T18:56:24.517 回答
4

我不确定 Emacs/coqtop 交互如何在这里发挥作用，但我相信确实存在 OCaml 顶级错误，应该在 OCaml bugtracker中报告。你准备好报告了吗？如果没有，我可以照顾它。

ocaml 和 coqtop 是否强制执行此字符限制？

顶层代码中有各种输入缓冲区，其中一些长度为 1024；快速查看代码后，有一个调整大小的逻辑，以防输入太大，所以它应该可以工作。我已经能够重现“不能在交互式顶层输入超过 N 个字符”的问题（不使用时rlwrap），但是限制为 N=4096 而不是 N=1024，所以我不确定它是否完全相同问题。

为什么只用于来自终端或 Emacs 的输入，而不是来自管道或文件的输入？

顶层代码区分了交互式和非交互式输入；iirc。例如，它会影响打印错误位置的方式。

为什么证明将军（显然）不知道这个限制会导致挂起错误和神秘的^Gs？

我不知道。coqtop您观察到的问题甚至可能是由类似缓冲逻辑引起的不同错误（不同于错误）。ocaml

我该如何解决这个限制？

在 Proof General 中不要一次发送太长的输入怎么样？也许您可以分解您的代码以使用中间定义或其他东西，以保持低于限制。

关于“上游修复”的情况：我相信 OCaml 和 Coq 都在很快获得新版本的过程中。如果人们对这个 bug 有足够的兴趣并很快得到一个真正的修复（特别是，如果你自己找到了修复），它可以相当快地集成到上游。否则，您将不得不等待下一个发布周期，并可能同时维护一个本地分支以避免该问题。务实地说，“通过改变我的 Coq 开发来解决”选择可能是最省力的解决方案，但它不会造福整个人类！

编辑：（回答评论）

我正在考虑的调整大小逻辑是 in Lexing.lex_refill， found in stdlib/lexing.ml，由创建的闭包Lexing.from_function调用，调用 from toplevel/toploop.ml。

我有另一个“解决方法”的想法：将您的长短语写入外部文件foo.v，并用于Load foo.获取顶层以读取文件本身。我怀疑这将解决大小限制，但尚未测试。

于 2012-07-05T08:35:10.800 回答