Edit 4：事实证明，这实际上只是一般TTY输入的限制;OCaml，Coq或Emacs没有任何具体的东西导致了这个问题。
<小时 />我正在开发一个在Emacs中使用Proof General的Coq程序，我发现了一个输入太长的错误。 如果通过 Proof General 提交给coqtop的区域包含超过 1023 个字符，则 Proof General（尽管不是 Emacs）在等待响应时挂起，并且 *coq* 缓冲区包含超过 1023 的每个字符一个额外的^G字符。 例如，如果将一个 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 个字符的行然后按 return 有效;但是在键入 1024 个字符后，点击任何键，包括返回（但不包括删除等），只会发出哔哔声。 事实证明，ocaml（OCaml 顶层）具有相同的行为：
perl -e 'print ((" " x 1024) . "1;;")' | ocaml
工作正常，但如果从终端运行ocaml，我不能在一行上键入超过 1024 个字符。 由于我的理解是coqtop依赖于OCaml顶层（当以coqtop -byte运行时更明显），我想这是一个相关的限制。
相关软件版本包括：
- 来自自制软件的OCaml 3.12.1;
- 来自Homebrew的Coq 8.3pl3（和8.3pl2）;
- 证明一般 4.1;
- 从 Emacs for Mac OS X 构建的 GNU Emacs 24.1.1;以及
- Mac OS X 10.6.7。
我的问题是：
ocaml和coqtop执行此字符限制呢？ 为什么只用于来自终端或 Emacs 的输入，而不是来自管道或文件的输入？- 为什么证明将军（明显）对这个限制的无知会导致悬挂错误和神秘的
^G？ - 如何解决此限制？ 我的最终目标是在 Proof General/Emacs 中使用 Coq，因此可以避免潜在问题的解决方法。
编辑 3：在发现 Ocaml 顶层中也存在 1024 个字符的输入限制（我想是相关的）后，我添加了该信息并删除了原始问题描述，因为它已被完全掩盖和取代。 （如有必要，请参阅编辑历史记录）。
我在 OCaml 错误跟踪器上将此报告为问题 5678，用户 dim 解释说这不是 OCaml 本身的问题，而是 TTY 输入的限制。 问题是这个。 由于在用户点击 return 之前，文本不会发送到正在运行的命令，因此所有等待的输入都必须存储在某个地方。 存储它的缓冲区（称为输入队列或提前键入缓冲区）具有固定大小，由 C 常量MAX_INPUT控制。 此常量在 Mac OS X 上等于 1024。 像这样的缓冲允许对输入进行有用的处理，例如在发送字符之前删除字符。 从终端运行的所有不执行特殊操作（例如使用 readline 库）的命令都将表现出此行为;例如，cat以完全相同的方式窒息。
为了避免这种行为，可以取消设置ICANON标志，例如通过运行stty -icanon;这会将TTY置于非规范输入模式，其中输入在发送到命令之前根本不处理。 这意味着编辑变得不可能：删除、左右箭头等都输入它们的文字等效项（^?、^[[D、^[[C、...）;同样，⌃D 不再发送 EOF，而只是发送文字控制字符。 然而，对于我的特定用例，这（到目前为止！）似乎是理想的，因为Emacs正在为我处理我的所有输入。 （编辑：但有一个更好的选择！ （据我了解，像readline这样的库也会更改此设置，但要注意控制字符并自行处理编辑等。 要恢复规范模式，可以运行 stty icanon .
ledit工具围绕作为参数提供给它的程序进行行编辑，因此ledit coqtop工作正常（如果奇怪;我更喜欢ledit -l 65536以避免它的滚动），但与Emacs的交互很奇怪。 rlwrap工具执行相同的操作，但让另一个程序从 TTY 读取;因此，虽然它可以接收更长的输入，但按 Enter 并将它们发送到包装的命令的行为非常奇怪，最终需要杀死命令。
编辑：在我的特定用例中，我也可以简单地告诉Emacs使用管道而不是PTY，一下子解决问题。 Emacs 变量process-connection-type控制如何与附属流程进行通信; nil表示使用管道，非nil表示使用TTY。 证明常规使用变量proof-shell-process-connection-type来确定应如何设置。 使用管道可以解决所有 1024 个字符限制的问题。
我不确定 Emacs/coqtop 交互在这里是如何发挥作用的，但我相信确实存在一个 OCaml 顶级错误，应该在 OCaml 错误跟踪器中报告。你准备好报告了吗？如果没有，我可以处理它。
ocaml 和 coqtop 执行此字符限制怎么样？
顶级代码中有各种输入缓冲区在起作用，其中一些长度为 1024;在快速查看代码后，有一个调整大小逻辑，以防输入变得太大，所以它应该可以工作。我已经能够重现"不能在交互式顶层中键入超过 N 个字符"问题（不使用 rlwrap 时），但限制为 N=4096 而不是 N=1024，所以我不确定这是完全相同的问题。
为什么只用于来自终端或 Emacs 的输入，而不是来自管道或文件的输入？
顶级代码区分了交互式和非交互式输入;例如，iirc.它会影响错误位置的打印方式。
为什么证明将军（明显）对这个限制的无知会导致挂起错误和神秘的^Gs？
我不知道。您观察到的coqtop问题甚至可能是由类似的缓冲逻辑引起的不同错误（与ocaml错误不同）。
如何解决此限制？
如何在证明常规中一次发送太长的输入？也许你可以分解你的代码以使用中间定义或其他东西，以保持在限制以下。
关于"上游修复"的情况：我相信OCaml和Coq都在尽快获得新版本。如果人们对该错误足够感兴趣以尽快获得修复（特别是，如果您自己找到修复程序），则可以相当快速地将其集成到上游。否则，您将不得不等待下一个发布周期，并可能同时维护本地分支以避免此问题。务实地说，"通过改变我的辅酶开发来变通"的选择可能是最省力的解决方案，但它不会造福整个人类！
编辑：（回答评论）
我想到的调整大小逻辑在Lexing.lex_refill中，在stdlib/lexing.ml中找到，由Lexing.from_function创建的闭包调用，从toplevel/toploop.ml调用。
我还有另一个"解决方法"的想法：将您的长短语写入外部文件foo.v，并使用Load foo.获取顶级来读取文件本身。我怀疑这将解决大小限制，但尚未测试。