Line length limitations in sertop

[riswords]

I'm seeing that in sertop, if I enter a very long command more than say 5,000 characters as a single line without line breaks, I'm seeing sertop hang with no response. If I then interrupt it, I can continue entering commands with no problems. I've also found that if I split my 5,000-character command up into multiple lines, then the command can be processed without a problem.

From further testing, it looks as though lines are getting truncated to 4,096 characters. I've found that commands split across lines shorter than that limit will succeed, and lines that are longer than that start producing errors. Further support for the line truncation theory: if I enter the full 5,000+ character command on a single line (so that sertop hangs), I can then enter a whole bunch of closing parentheses to trigger a Sexplib.Conv.Of_sexp_error, so sertop isn't really hanging per se; it's truncated the input and is still waiting for the end of the expression.

My specific example won't lend itself well to reproducibility due to dependencies, but all I'm doing is trying to use Print on a (very) large AST:

(Print () (CoqAst [large AST]))

where the CoqAst is a result of running (Query () (Ast [stateid])).

Ideally, it would be nice if sertop didn't have this line length limit at all, or if it could show an error message when the limit is exceeded.

[ejgallego]

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.

[ejgallego]

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.

[ejgallego]

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

[ejgallego]

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