readFile omits parts of the file

Stream: lean4

[Eric Wieser]

I was pretty surprised to discover this:

#eval do
  let path := "/tmp/lean-zulip-example"
  IO.FS.writeBinFile path
    ("Hello\x00(this is a very secret message that must never be shared) world".toUTF8)
  let x ← IO.FS.readFile path
  IO.println x

[Eric Wieser]

(lean4#4891)

[Eric Wieser]

(sorry for the edits, I over-minimized this to begin with)

[Mac Malone]

Yep, this was fun to discover while validating Lake's TOML parser. Interesting, this behavior is noted in the comments of the C get line funciton, but nowhere in the Lean code.

[Henrik Böving]

I have a fix for it, will PR next week

[Henrik Böving]

https://github.com/leanprover/lean4/pull/4906