fix: remove broken Handle.isEof

src/Init/System/IO.lean

@@ -220,7 +220,6 @@ opaque FS.Handle : Type := Unit
   A pure-Lean abstraction of POSIX streams. We use `Stream`s for the standard streams stdin/stdout/stderr so we can
   capture output of `#eval` commands into memory. -/
 structure FS.Stream where
-  isEof   : IO Bool
   flush   : IO Unit
   read    : USize → IO ByteArray
   write   : ByteArray → IO Unit
@@ -266,12 +265,6 @@ private def fopenFlags (m : FS.Mode) (b : Bool) : String :=
 def mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : IO Handle :=
   mkPrim fn (fopenFlags Mode bin)
 
-/--
-Returns whether the end of the file has been reached while reading a file.
-`h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
-Once `h.isEof` is true, reading `h` will always return an empty array.
--/
-@[extern "lean_io_prim_handle_is_eof"] opaque isEof (h : @& Handle) : BaseIO Bool
 @[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit
 /--
 Read up to the given number of bytes from the handle.
@@ -622,7 +615,6 @@ namespace Stream
 
 @[export lean_stream_of_handle]
 def ofHandle (h : Handle) : Stream := {
-  isEof   := Handle.isEof h,
   flush   := Handle.flush h,
   read    := Handle.read h,
   write   := Handle.write h,
@@ -635,7 +627,6 @@ structure Buffer where
   pos  : Nat := 0
 
 def ofBuffer (r : Ref Buffer) : Stream := {
-  isEof   := do let b ← r.get; pure <| b.pos >= b.data.size,
   flush   := pure (),
   read    := fun n => r.modifyGet fun b =>
     let data := b.data.extract b.pos (b.pos + n.toNat)

src/Lean/Data/Lsp/Communication.lean

@@ -39,7 +39,7 @@ section
 
   private partial def readHeaderFields (h : FS.Stream) : IO (List (String × String)) := do
     let l ← h.getLine
-    if (←h.isEof) then
+    if l.isEmpty then
       throw $ userError "Stream was closed"
     if l = "\r\n" then
       pure []

tests/lean/run/IO_test.lean

@@ -28,14 +28,8 @@ withFile "foo.txt" Mode.read fun h => do
     check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList
     let ys ← h.read 2
     check_eq "3" [7,8] ys.toList
-    let b ← h.isEof
-    unless !b do
-      throw $ IO.userError $ "wrong (4): "
     let ys ← h.read 2
     check_eq "5" [] ys.toList
-    let b ← h.isEof
-    unless b do
-      throw $ IO.userError $ "wrong (6): "
 pure ()
 
 #eval test
@@ -69,9 +63,6 @@ let ys ← withFile fn2 Mode.read $ fun h => do
     { let ln ← h.getLine;
       IO.println i;
       IO.println ∘ repr $ ln;
-      let b  ← h.isEof;
-      unless i == 1 || !b do
-        throw $ IO.userError "isEof"
       pure ln };
     pure ys };
 IO.println ys;
@@ -115,4 +106,4 @@ check_eq "1" [] ys.toList
 let ys ← withFile fn4 Mode.read $ fun h => h.read 1;
 check_eq "2" [] ys.toList
 
-#eval test4
+#eval test4