Невозможно предоставить длинные (более 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 процесс (либо с помощью Cc Cx или kill/killall из терминала).

Что-то об этом ограничении возникает из coqtop сам. Если один генерирует строку длиной 1024 символа или более и передает ее, например, запустив

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

тогда все работает нормально. (Так же, coqc хорошо работает также.) Однако, если я бегу coqtop в терминале я не могу набрать более 1024 символов в одной строке, включая завершающий символ возврата. Таким образом, ввод строки длиной 1023 символа, а затем нажатие клавиши return работает; но после ввода 1024 символов нажатие любой клавиши, включая возврат (но не удаление и т. д.), ничего не дает, кроме звукового сигнала. И получается, что ocaml (уровень OCaml) имеет такое же поведение:

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

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

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

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

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

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

Источник

2 ответа

Решение

Я сообщил об этом как о проблеме 5678 на трекере ошибок OCaml, и пользователь dim объяснил, что это не проблема с OCaml как таковая, а ограничение ввода TTY. Проблема заключается в следующем. Поскольку текст не отправляется в запущенные команды до тех пор, пока пользователь не нажмет return, все эти ожидающие данные должны где-то храниться. Буфер, в котором он хранится, называется входной очередью или буфером опережающего ввода, имеет фиксированный размер, который контролируется константой C MAX_INPUT, Эта константа равна 1024 в Mac OS X. Подобная буферизация позволяет выполнять полезную обработку ввода, например удалять символы перед их отправкой. Все команды запускаются из терминала, которые не делают ничего особенного (например, использование readline библиотека) будет демонстрировать это поведение; например, cat задыхается точно так же.

Чтобы избежать такого поведения, можно сбросить ICANON флаг, например, запустив stty -icanon; это переводит TTY в неканонический режим ввода, где ввод вообще не обрабатывается перед отправкой в ​​команду. Это означает, что редактирование становится невозможным: удаление, стрелка влево и вправо и т. Д. Все вводят свои буквенные эквиваленты (^?, ^[[D, ^[[C,…); Точно так же, longerD больше не посылает 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 символа.

Источник

Я не уверен, как здесь взаимодействует Emacs/coqtop, но я полагаю, что действительно существует ошибка верхнего уровня OCaml, и о ней следует сообщить в багтрекер OCaml. Вы были бы готовы сообщить об этом? Если нет, я могу позаботиться об этом.

Как насчет ocaml и coqtop применяет этот лимит символов?

В коде верхнего уровня присутствуют различные входные буферы, некоторые из которых имеют длину 1024; после быстрого взгляда на код, существует логика изменения размера на случай, если ввод становится слишком большим, поэтому он должен работать. Мне удалось воспроизвести проблему "не могу набрать больше, чем N символов в интерактивном верхнем уровне" (когда я не использовал rlwrap), но с пределом N=4096, а не N=1024, поэтому я не уверен, что это та же самая проблема.

И почему только для ввода из терминала или Emacs, в отличие от ввода из канала или файла?

Код верхнего уровня делает различие между интерактивным и неинтерактивным вводом; IIRC. например, это влияет на то, как печатаются места ошибок.

Почему (очевидное) игнорирование этого предела Генеральным прокурором приводит к ошибкам и загадочным ^Gs?

Я понятия не имею. coqtop проблема, которую вы наблюдаете, может даже быть другой ошибкой (чем ocaml 1) вызвано аналогичной логикой буферизации.

Как я могу обойти это ограничение?

Как насчет того, чтобы не отправлять слишком длинные входы сразу в Proof General? Может быть, вы можете факторизовать свой код, чтобы использовать промежуточные определения или что-то еще, чтобы остаться ниже предела.

Что касается ситуации с исправлением исходных данных: я полагаю, что и OCaml, и Coq скоро получат новую версию. Если люди достаточно заинтересованы в этой ошибке, чтобы исправить ее в ближайшее время (в частности, если вы найдете ее самостоятельно), она может быть достаточно быстро интегрирована в апстрим. В противном случае вам придется ждать следующего цикла выпуска и, возможно, поддерживать локальный форк тем временем, чтобы избежать этой проблемы. С практической точки зрения, "обходной путь, меняющий мой Coq development" - это, вероятно, решение с минимальными усилиями, но оно не принесет пользы человечеству в целом!

Изменить: (чтобы ответить на комментарии)

Логика изменения размера, о которой я думал, находится в Lexing.lex_refill, нашел в stdlib/lexing.mlвызывается замыканием, созданным Lexing.from_functionпозвонил из toplevel/toploop.ml,

У меня есть еще одна "обходная" идея: написать длинную фразу во внешний файл foo.vи использовать Load foo. чтобы получить верхний уровень для чтения самого файла. Я подозреваю, что это будет работать вокруг ограничения размера, но не проверял.

Источник
Другие вопросы по тегам