7

編集 4 : これは、実際には一般的な TTY 入力の制限にすぎないことがわかりました。問題の原因となっている OCaml、Coq、または Emacs については特に何もありません。

Emacs で Proof General を使用して Coq プログラムに取り組んでいますが、入力が長すぎるバグを発見しました。Proof Generalを介して送信する領域にcoqtop1023 文字を超える文字が含まれている場合、Proof General (Emacs ではありません) は応答を待っている間にハングし、*coq*バッファーには^G1023 文字を超える文字ごとに 1 つの余分な文字が含まれます。たとえば、1025 文字の場合region が に送信されたcoqtop場合、*coq*バッファは 2 つの余分な文字で終了し^G^Gます。ファイルのこのポイントを超えて先に進むことができず、coqtopプロセスを強制終了する必要があります (C-c C-xまたはターミナルからkill/を使用killall)。

この制限に関する何かは、coqtopそれ自体から生じます。1024文字以上の文字列を生成し、それをパイプする場合

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

その後、すべて正常に動作します。(同様に、正常にcoqc動作します。) しかし、ターミナルで実行するcoqtopと、1 行に 1024 文字を超える文字を入力できません。これには、最後の改行文字が含まれます。したがって、1023 文字の行を入力してから改行を押すと機能します。しかし、1024 文字を入力した後、return を含む (delete などは含まない) 任意のキーを押しても、ビープ音が鳴るだけです。そして、ocaml(OCaml トップレベル) が同じ動作をすることがわかりました:

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

ocaml正常に動作しますが、端末から実行している場合、1 行に 1024 文字を超える文字を入力できません。私の理解ではcoqtop、OCaml のトップレベルに依存しているため (より明らかに as として実行した場合coqtop -byte)、これは関連する制限であると思います。

関連するソフトウェア バージョンは次のとおりです。

そして私の質問は次のとおりです。

  • この文字数制限の実施ocamlについてはどうですか? coqtopそして、なぜパイプやファイルからの入力ではなく、端末や Emacs からの入力だけなのですか?
  • Proof General がこの制限を (明らかに) 無知であるために、エラーがハングしたり、謎^Gの s が発生したりするのはなぜですか?
  • この制限を回避するにはどうすればよいですか? 私の最終目標は、Proof General/Emacs 内で Coq を使用することなので、根本的な問題を回避する回避策は問題ありません。

編集 3: 1024 文字の入力制限が Ocaml トップレベルにも存在することを発見した後 (関連していると思われるもの)、その情報を追加し、元の問題の説明を削除しました。(必要に応じて編集履歴を参照してください)。

4

2 に答える 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 から読み取ったままになります。したがって、より長い入力を受け取ることはできますが、Enter キーを押してラップされたコマンドに送信すると、非常に奇妙な動作になり、最終的にはコマンドを強制終了する必要があります。

編集：私の特定のユースケースでは、EmacsにPTYの代わりにパイプを使用するように指示するだけで、問題を一気に解決することもできます。Emacs 変数process-connection-typeは、補助プロセスとの通信方法を制御します。nilはパイプを使用することをnil意味し、non- は TTY を使用することを意味します。Proof General は変数proof-shell-process-connection-typeを使用して、これをどのように設定するかを決定します。パイプを使用すると、1024 文字制限の問題がすべて解決されます。

于 2012-07-11T18:56:24.517 に答える