Невозможно предоставить длинные (1024+ символа )входные данные для верхнего уровня OCaml и coqtop (и Proof General)

Редактировать 4:Оказывается, на самом деле это просто ограничение ввода TTY в целом; в OCaml, Coq или Emacs нет ничего конкретного, что вызывает проблему.

Я работаю над программой Coq, используя Proof General в Emacs, и обнаружил ошибку со слишком длинным вводом. Если область для отправки в 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

работает отлично,но я не могу ввести более 1024 символов в одной строке при запуске ocamlс терминала. Поскольку я понимаю, что coqtopполагается на верхний уровень OCaml (более очевидно при запуске какcoqtop -byte), я полагаю, что это связанное ограничение.

Соответствующие версии программного обеспечения::

• OCaml 3.12.1 из Homebrew ;
• Coq 8.3pl3 (и 8.3pl2 )из Homebrew ;
• Общее доказательство 4.1;
• Сборка GNU Emacs 24.1.1 из Emacs для Mac OS X ; и
• Mac OS X 10.6.7.

И мои вопросы:

• Что насчет ocamlи coqtopобеспечивает соблюдение этого ограничения на количество символов? И почему только для ввода из терминала или Emacs, а не для ввода из канала или файла?
• Почему очевидное )игнорирование Proof General (этого предела приводит к ошибкам зависания и таинственным ^Gs?
• Как я могу обойти это ограничение? Моя конечная цель — использовать Coq внутри Proof General/Emacs, поэтому обходные пути, позволяющие избежать основной проблемы, вполне приемлемы.

Редактировать 3:Обнаружив, что ограничение на ввод 1024 -символов также существует на верхнем уровне Ocaml (, что, как мне кажется, связано ), я добавил эту информацию и удалил исходное описание проблемы, так как оно было полностью скрыто и заменено. (См. историю редактирования при необходимости ).