logo标签列表

无法向OCaml顶层、coqtop（以及Proof General）提供长达1024个字符以上的输入。

emacsocamlttycoqproof-general
7

编辑4: 原来这只是TTY输入的限制; 没有OCaml、Coq或Emacs导致问题。

我正在使用Emacs中的Proof General编写Coq程序，发现了一个输入太长的错误。如果提交给coqtop的区域通过Proof General包含超过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

如果我在终端中运行coqtop，每行最多只能输入1024个字符，包括回车符。因此，输入1023个字符后按回车键是可以的；但是，在输入1024个字符后，按任何键（包括回车键，但不包括删除键等）都只会发出哔声而没有其他反应。同样地，coqc也可以正常工作。事实证明，ocaml（OCaml顶层）也具有相同的行为：

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

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

相关软件版本如下：

我的问题是：

  • 是什么导致了 ocaml 和 coqtop 的字符限制？为什么只对来自终端或Emacs的输入有效，而不对来自管道或文件的输入有效？
  • 为什么Proof General（显然）无视这个限制会导致挂起错误和神秘的 ^G？
  • 如何解决这个限制？我的最终目标是在Proof General/Emacs中使用Coq，因此可以规避基本问题的解决方法是可以接受的。

编辑3：发现1024个字符输入限制也存在于Ocaml toplevel中（我想这是相关的），因此我添加了该信息并删除了原始问题描述，因为它已完全被掩盖和取代。（如果需要，可以查看编辑历史记录）。

2个回答
5
我在OCaml错误跟踪器上报告了这个问题，编号为5678，用户dim解释说这不是OCaml本身的问题，而是TTY输入的限制。问题在于，由于文本直到用户按回车键才被发送到正在运行的命令，所有等待输入的内容都必须存储在某个地方。它存储在称为输入队列或类型前缀缓冲区的缓冲区中，其大小由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 中读取数据；因此，尽管它可以接收更长的输入，但按下回车键并将其发送到被包装的命令时会表现得非常奇怪，并最终导致必须杀死该命令。 编辑： 在我的特定用例中，我还可以告诉 Emacs 使用管道而不是 PTY，一举解决所有问题。Emacs 变量 process-connection-type 控制如何与子进程通信；nil 表示使用管道，而非 nil 则表示使用 TTY。Proof General 使用变量 proof-shell-process-connection-type 来确定应该如何设置。使用管道可以解决所有 1024 字符限制的问题。
4
我不确定Emacs / coqtop的交互在这里扮演了什么角色，但我相信确实存在一个OCaml toplevel bug，并且应该在OCaml bugtracker中报告。你准备好报告吗？如果没有，我可以处理它。
关于ocaml和coqtop，是什么导致了这个字符限制？
在toplevel代码中有各种输入缓冲区，其中一些长度为1024；经过快速查看代码后，如果输入过大，会有一个调整大小的逻辑，所以它应该能够工作。我已经能够重现“无法在交互式toplevel中输入超过N个字符”的问题（当不使用rlwrap 时），但是N = 4096而不是N = 1024，因此我不确定是否是完全相同的问题。
那么为什么只对来自终端或Emacs的输入强制执行此限制，而不是来自管道或文件的输入？
toplevel代码区分交互式和非交互式输入；我记得它影响打印错误位置的方式，例如。
为什么Proof General（明显）对此限制的无知会导致悬挂错误和神秘的^G？
我不知道。您观察到的coqtop问题甚至可能是一个与ocaml不同的bug，由类似的缓冲逻辑引起。 如何解决这个限制？
在Proof General中发送时不要一次发送过长的输入。也许您可以将代码分解为使用中间定义之类的内容，以保持低于限制。
关于“上游修复”情况：我相信，OCaml和Coq都正在很快地获得新版本。如果人们对该漏洞足够感兴趣，并且想马上得到修复（特别是如果您自己找到了解决方法），则可以合理快速地集成到上游。否则，您将不得不等待下一个发布周期，并可能在此期间维护本地分支以避免出现问题。从实用角度来看，“通过更改我的Coq开发来解决问题”的选择可能是最低投入的解决方案，但它不会使整个人类受益！
编辑：（回答评论）

我想到的调整大小逻辑在stdlib/lexing.ml中的Lexing.lex_refill中，由Lexing.from_function创建的闭包调用，该闭包由toplevel/toploop.ml调用。

我有另一个"解决方法"的想法：将您的长语句写入一个外部文件foo.v，然后使用Load foo.让toplevel读取文件本身。我猜这将绕过大小限制，但尚未进行测试。

非常好的回答，谢谢！有几个问题。首先，我可以提交这个漏洞；感谢提供链接。你在哪个文件中找到了缩放逻辑？第二，我发现rlwrap让我可以输入更多字符，但在提交时会出错。第三：重构是一个选择，但只能做到一定程度。如果我的Inductive定义很长，我不能有效地将其分成多个较小的数据类型 :-/所以希望我能找到实际的解决方法。 - Antal Spector-Zabusky
仅供记录，我已在跟踪器上报告了问题issue 5678。不幸的是，调整大小逻辑似乎并不是导致问题的原因。 - Antal Spector-Zabusky
事实证明这个故障与OCaml无关。我已经将从错误报告中获得的信息添加为答案。感谢您的帮助！ - Antal Spector-Zabusky
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接