无法为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 toplevel)具有相同的行为:

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

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

相关软件版本是:

• 来自Homebrew的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的输入,而不是来自管道或文件的输入？
• 为什么Proof General(明显)对这个限制的无知导致悬挂错误和神秘^Gs？
• 我该如何解决这个限制？我的最终目标是在Proof General/Emacs中使用Coq,因此避免潜在问题的解决方法很好.

---

编辑3:在发现Ocaml顶层中存在1024个字符的输入限制(我想象的是相关的)之后,我添加了该信息并删除了原始的问题描述,因为它已被完全模糊和取代.(如有必要,请参阅编辑历史记录).

Answer 1

我在OCaml错误跟踪器上报告了这个问题5678,并且用户昏暗地解释说这不是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个字符限制问题.