lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

feat: blocking behavior on EOF for readLine

Open goens opened this issue 3 years ago • 1 comments

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.

goens avatar Aug 14 '22 13:08 goens

Thanks for your contribution! Please make sure to follow our Commit Convention.

github-actions[bot] avatar Aug 14 '22 13:08 github-actions[bot]