Line length limitations in sertop about coq-serapi HOT 4 CLOSED

Thanks for the report, will investigate the issue as soon as I get the ppx toolchain working again [c.f. ocaml-ppx/ppx_import#17]

Note that in Query you can set the output options so you can do (Query ((pp ((pp_format PpStr)))) (Ast sid)) to avoid this problem.

It will be also possible to store the outputs of querys in "views", that can then be forwarded to other commands and avoid the roundtrip.

from coq-serapi.

It turns out that the 4k input limitation is coming from the TTY, see https://unix.stackexchange.com/questions/131105/how-to-read-over-4k-input-without-new-lines-on-a-terminal for example.

I am keeping this issue open until I figure out what is the best way to read long files from the terminal, but using a pipe to sertop you should be able to overcome this limitation.

from coq-serapi.

Closing this as invalid and it is really a tty problem, documenting in the FAQ.

from coq-serapi.

Note that you can use the (ReadFile "file.v") hack to make your life easier.

from coq-serapi.