emacs - 无法向 OCaml 顶层和 coqtop(和 Proof General)提供长(1024+ 个字符)输入

Question

编辑 4 : 事实证明，这实际上只是一般的TTY输入的限制；没有任何关于 OCaml、Coq 或 Emacs 的特定原因导致问题。

我正在 Emacs 中使用 Proof General 开发 Coq 程序，但我发现输入过长的错误。如果一个地区提交到coqtop通过 Proof General 包含超过 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 3.12.1 来自 Homebrew ;

Coq来自 Homebrew 的 8.3pl3(和 8.3pl2) ;

Proof General 4.1;

GNU Emacs的构建24.1.1 来自 Emacs for Mac OS X ;和

Mac OS X 10.6.7。

我的问题是:

怎么样ocaml和 coqtop是否强制执行此字符限制？为什么只针对来自终端或 Emacs 的输入，而不是来自管道或文件的输入？

为什么 Proof General 对这个限制的(明显)无知会导致挂起错误和神秘 ^G ?

我该如何解决这个限制？我的最终目标是在 Proof General/Emacs 中使用 Coq，因此可以避免潜在问题的解决方法。

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

Answer 1

我将此报告为 issue 5678在 OCaml 错误跟踪器上，用户 dim 解释说这不是 OCaml 本身的问题，而是 TTY 输入的限制。问题是这个。由于文本在用户点击返回之前不会发送到运行命令，因此所有等待的输入必须存储在某个地方。存储它的缓冲区，称为输入队列或提前输入缓冲区，具有固定大小，由 C 常量 MAX_INPUT 控制。 . This constant is equal to 1024 on Mac OS X .像这样的缓冲允许有用的输入处理，例如在发送之前删除字符。从终端运行的所有命令(例如使用 readline 库)不做任何特殊的事情都会表现出这种行为；例如，cat以完全相同的方式窒息。

为了避免这种行为，可以取消设置 ICANON标志，例如通过运行 stty -icanon ;这会将 TTY 放入 non-canonical input mode ，其中在发送到命令之前根本不处理输入。这意味着编辑变得不可能:删除、向左和向右箭头等都输入它们的字面等效项( ^? 、 ^[[D 、 ^[[C 、...)；类似地， ⌃D 不再发送 EOF，而只是一个文字控制字符。然而，对于我的特定用例，这(到目前为止!)似乎是理想的，因为 Emacs 正在为我处理我的所有输入。 ( 编辑: 但有更好的选择!)(像 readline 这样的库，据我所知，也更改此设置，但要注意控制字符和处理编辑等，它们自己。)恢复规范模式，可以运行 stty icanon .

ledit 工具将行编辑环绕作为参数提供给它的程序，因此 ledit coqtop工作正常(如果奇怪；我更喜欢 ledit -l 65536 以避免滚动)，但与 Emacs 交互很奇怪。 rlwrap tool 做同样的事情，但让另一个程序从 TTY 读取；因此，虽然它可以接收更长的输入，但按 Enter 并将它们发送到包装的命令的行为非常奇怪，最终需要终止该命令。

编辑:在我的特定用例中，我也可以简单地告诉 Emacs 使用管道而不是 PTY，从而一举解决问题。 Emacs 变量 process-connection-type 控制如何与附属过程通信； nil表示使用管道，非 nil表示使用 TTY。 Proof General 使用变量 proof-shell-process-connection-type 以确定应如何设置。使用管道可以解决所有 1024 个字符限制的问题。