lean4-cli

Stream: lean4

[Marc Huisinga]

A small library to help build command line interfaces in Lean 4: https://github.com/mhuisi/lean4-cli

I hope that this helps with improving the tooling.

[Arthur Paulino]

This lib is amazing. Thank you very much for the work :octopus:
An idea I just had is to provide a NOOP as syntax sugar for VIA fun _ => pure 0 when you want a command to only have sub-commands and do nothing by itself

[Arthur Paulino]

Another idea... maybe this line should use IO.eprintln instead

[Marc Huisinga]

Thanks! These are both good suggestions. I'll push them to the nightly branch soon.

[Hanting Zhang]

@Marc Huisinga We're running into a weird bug

application type mismatch
  Cli.Flag.mk "p"
argument
  "p"
has type
  String : Type
but is expected to have type
  Option String : Type

I don't believe it's an error on cli's part, but something strange going on with the typeclass search that is failing to find the A -> Option A coe. The context is too complicated to replicate, so I won't show the code here, but it will work/not work depending randomly (?) on what imports we have.

Anyways, would it be possible to add a tiny fix making this Option coe explicit? Literally just

expandIdentLiterally flag[0]
-- fix
← `(some $(expandIdentLiterally flag[0]))

in expandFlag.

[Marc Huisinga]

I'll take a closer look later, but at first sight this seems like a reasonable fix (the macro shouldn't generate coercions anyways, I must have missed that one)

[Marc Huisinga]

@Hanting Zhang This should be fixed now. Please let me know if the issue persists.

[Hanting Zhang]

Thank you! I'll let you know how it goes