lean4
lean4 copied to clipboard
feat: blocking behavior on EOF for readLine
As discussed in Zulip, this implements the blocking behavior seen by Rust. When a stream sees an EOF on a readLine, it will return an empty string once. When called again, it will read the input again, instead of immediately returning an empty string again.
Currently there's no test, as we need to control stdin for that. I have a simple test that works for this, but relies on [expect](https://en.wikipedia.org/wiki/Expect:
def main : IO Unit := do
IO.println "input a line"
let input <- (← IO.getStdin).getLine
println! "input length: {input.length}"
let input <- (← IO.getStdin).getLine
println! "input length: {input.length}"
let input <- (← IO.getStdin).getLine
println! "input length: {input.length}"
and
#!/opt/homebrew/bin/expect -f
set force_conservative 0 ;# set to 1 to force conservative mode even if
;# script wasn't run conservatively originally
if {$force_conservative} {
set send_slow {1 .1}
proc send {ignore arg} {
sleep .1
exp_send -s -- $arg
}
}
set timeout -1
spawn ./build/bin/test
match_max 100000
expect -exact "input a line\r
"
send -- ""
expect -exact "input length: 0\r
"
send -- "a\r"
expect -exact "a\r
input length: 2\r
"
send -- "a\r"
expect eof
Happy to include it if wanted.
Thanks for your contribution! Please make sure to follow our Commit Convention.