Exercise 2.4 Functional Programming in Lean 4

Stream: lean4

[Austin Anderson]

Does anyone have a solution to the "--help" exercise in section 2.4? Among other things, I tried the code below where everything except lines 4-7 is from the textbook. One problem I'm getting is IO Unit and IO UInt32 are mismatched types and I don't know how to put a message like "you want help" in type IO UInt32. Thanks!

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
match args with
| [] => pure exitCode
| "--help" :: args =>
let stdout ← s!"You want help!"
dump stdout
process exitCode args
| "-" :: args =>
let stdin ← IO.getStdin
dump stdin
process exitCode args
| filename :: args =>
let stream ← fileStream ⟨filename⟩
match stream with
| none =>
process 1 args
| some stream =>
dump stream
process exitCode args

[Henrik Böving]

Please use #backticks for your code. Note that there is no need to put the string into the IO monad, you can just use a normal let binding: let stdout := "You want help!"

[Austin Anderson]

Thank you. So below is the whole thing, all but 3 lines copied from Functional Programming in Lean section 2.4. And it gives an error when I type

lake build

in terminal. The error is below that.

def bufsize : USize := 20*1024
partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not fizzound: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "--help" :: args =>
    let stdout := "You want help!"
    dump stdout
    process exitCode args
  | "-" :: args =>
    let stdin ← IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream ← fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ => process 0 args
```

```
```quote
error: ././././Main.lean:25:18: type mismatch
  toString "You want help!"
has type
  String : Type
but is expected to have type
  IO ?m.1151 : Type
error: Lean exited with code 1
Some builds logged failures:
- Main
error: build failed
```

[Kim Morrison]

I'm confused. There is no toString "You want help!" in your code. When I open your code in the sandbox I see:

application type mismatch
  dump stdout
argument
  stdout
has type
  String : Type
but is expected to have type
  IO.FS.Stream : Type

instead.

[Austin Anderson]

Thanks for the reply. I had a line that said

but per Henrik's comment I changed it to

let stdout := "You want help!"

I have tried multiple things, but really just wonder what David Thrane Christiansen had in mind for the exercise he wrote. Perhaps something not fully covered in the book section is required.

[Austin Anderson]

sorry retry. I had

let stdout ← s!"You want help!"

[Paul Rowe]

I think the idea of the exercise is to make it a slightly more realistic program by making it act the way many command line programs do. For example, if you type code --help on the command line, the effect is to print a bunch of information about how to use the code command. It's a simple way to document the intended usage and list of available command line options.

So when you type <prog_name> --help this should have the effect of printing this documentation to stdout and returning a UInt32 to indicate success (usually 0).

[Austin Anderson]

Thank you. I agree. But I think a simple message like "you want help!" is a start, and since I cannot even get that to work, I'm at a loss.

[Kim Morrison]

Could you post the code you have so far, with #backticks and error messages matching the code?

[David Thrane Christiansen]

I don't want to just post a solution, but here's a hint.

It looks to me like you're using stdout as the name of the text that is to be sent to standard output. But the intention in the chapter is that stdout refers to the Lean representation of the stdout file descriptor/output stream - that is, it's a place to which streams can be sent.

The dump function expects to take an input stream as its argument, and it then loops until the stream runs out of data, sending its contents to standard output. Presumably, this is not something that should be done when users ask for help, because those users aren't looking to actually concatenate any streams.

Here's a program that isn't feline, but that does have a help message. See if you can figure out how it's doing what it does, and then adapt it to the exercise's other argument handling:

def main (args : List String) : IO UInt32 := do
  match args with
  | [] =>
    IO.println "OK"
    return 0
  | ["--help"] =>
    IO.println "Usage information:"
    IO.println "    --help    Show this usage information"
    IO.println ""
    IO.println "Run with no arguments to complete successfully."
    return 1
  | arg :: _ =>
    IO.eprintln s!"Didn't understand argument \"{arg}\""
    return 2

[François G. Dorais]

Another hint might be <https://github.com/leanprover/lean4-cli>

[Austin Anderson]

Thank you very much! My original attempt now works. I know its cheekily incomplete, but I learned a lot and understand at least one way it could be completed. When I type .lake/build/bin/feline --help test1.txt test2.txt I get

You want help!
Time to find a warm spot
and curl up.

Thanks very much for writing the book! I'm a math guy and have only used Lean to formalize math so far, but I'm trying to understand LeanDojo and LLMStep for which I find your book extremely helpful. My hero!
My code is below.

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not fizzound: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "--help" :: args =>
    IO.println "You want help!"
    process exitCode args
  | "-" :: args =>
    let stdin ← IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream ← fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ => process 0 args

[Austin Anderson]

(deleted)