REPL Gets Stuck With Long Inputs

[yangky11]

Hello, I have a problem with the sertop REPL.
It gets stuck when I copy-and-paste a very long command into sertop. The same issue happens also when I try to interact with sertop using a pseudo-terminal in a Python program.
But it is OK if I pass the command via a pipe (echo $a_long_command | sertop) .
So I guess it's related to how keyboard input is handled. Any idea? Thanks.

An example command is :

(Add () "Check fun c : comparison => match c as c0 return (forall c' : comparison, ~ c0 <> c' -> c0 = c') with | Eq => fun c' : comparison => match c' as c0 return (~ Eq <> c0 -> Eq = c0) with | Eq => fun _ : ~ Eq <> Eq => eq_refl | Lt => fun H : ~ Eq <> Lt => let n : False := H (fun H0 : Eq = Lt => let H1 : False := eq_ind Eq (fun e : comparison => match e with | Eq => True | _ => False end) I Lt H0 in False_ind False H1) in match n return (Eq = Lt) with end | Gt => fun H : ~ Eq <> Gt => let n : False := H (fun H0 : Eq = Gt => let H1 : False := eq_ind Eq (fun e : comparison => match e with | Eq => True | _ => False end) I Gt H0 in False_ind False H1) in match n return (Eq = Gt) with end end | Lt => fun c' : comparison => match c' as c0 return (~ Lt <> c0 -> Lt = c0) with | Eq => fun H : ~ Lt <> Eq => let n : False := H (fun H0 : Lt = Eq => let H1 : False := eq_ind Lt (fun e : comparison => match e with | Lt => True | _ => False end) I Eq H0 in False_ind False H1) in match n return (Lt = Eq) with end | Lt => fun _ : ~ Lt <> Lt => eq_refl | Gt => fun H : ~ Lt <> Gt => let n : False := H (fun H0 : Lt = Gt => let H1 : False := eq_ind Lt (fun e : comparison => match e with | Lt => True | _ => False end) I Gt H0 in False_ind False H1) in match n return (Lt = Gt) with end end | Gt => fun c' : comparison => match c' as c0 return (~ Gt <> c0 -> Gt = c0) with | Eq => fun H : ~ Gt <> Eq => let n : False := H (fun H0 : Gt = Eq => let H1 : False := eq_ind Gt (fun e : comparison => match e with | Gt => True | _ => False end) I Eq H0 in False_ind False H1) in match n return (Gt = Eq) with end | Lt => fun H : ~ Gt <> Lt => let n : False := H (fun H0 : Gt = Lt => let H1 : False := eq_ind Gt (fun e : comparison => match e with | Gt => True | _ => False end) I Lt H0 in False_ind False H1) in match n return (Gt = Lt) with end | Gt => fun _ : ~ Gt <> Gt => eq_refl end end.")

Another example:

(Add () "this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.this is a very long command.")

[yangky11]

I just noticed the same issue happen for coqtop as well.

[ejgallego]

Duplicate of #38