CLI library design

Stream: lean4

[Henrik Böving]

What's your opinion on CLI library design for Lean 4? I'm not aware of anything yet and would like to write a proper CLI for doc-gen4 but phase that out into a library.

The designs I'm aware of generally are:

• C style getopt which seems pretty primitive here
• Rust clap.rs style struct + macro based approach
• Haskell's optparse-applicative https://hackage.haskell.org/package/optparse-applicative which is probably the most functionally designed out of these
• docopt http://docopt.org/ style doc string based ones

Which of these do you think would be the best fit for lean? With the meta programming capabilities it should definitely not be an issue to implement either of these but I'm wondering what you think would be the most idiomatic to implement.

[Mario Carneiro]

I think the clap macro approach makes more sense than the haskell applicative stuff. There isn't really a need for using higher order functions (with lots of sigils) to get a nice interface when a macro can more directly express the desired input syntax as well as being able to produce values in structs made just for the purpose, or even structs constructed by the macro itself like rust structopt

[Mario Carneiro]

clap is a really full featured library though (to the point that you can usually see it in compile times). You probably want to trim that down a bit for an initial implementation

[Henrik Böving]

Hmmm, so this would require attributes in field declarations right? This does however not seem possible right now so I guess a good point to start would be to try and add this to the structure elaborator? I'd imagine we could just tag the resulting projection functions with the attributes right?

[Mario Carneiro]

No, it would use a custom syntax unrelated to structure

[Mario Carneiro]

although you can make it visually resemble a structure declaration if you want

[Mario Carneiro]

although I should point out that field declarations can actually have attributes

[Henrik Böving]

image.png my Lean does not seem to believe so.

[Mario Carneiro]

well, at least syntactically

[Henrik Böving]

Ah yes, the error is from the elaborator.

[Mario Carneiro]

which for a macro is really all you need

[Mario Carneiro]

I believe attributes in that position are intended to work in the future, that error looks like a todo

[Henrik Böving]

In that case why make up a different macro language?

[Mario Carneiro]

I'm not sure that structure + attributes is actually the best way to express requirements here. It's done that way in rust because it's a limitation of how attribute macros work

[Henrik Böving]

Do you have another "vision" for how one could express them then? If yes please do share

[Mario Carneiro]

The macro is deprecated now for clap v3 but clap v2 includes a clap_app! macro which expresses the same information in a very different way. It ends up looking more like the help text

[Mario Carneiro]

Here's an example of use from my project: https://github.com/digama0/mm0/blob/master/mm0-rs/src/main.rs#L5-L39

[Patrick Massot]

See also https://github.com/mhuisi/lean4-cli

[Patrick Massot]

From @Marc Huisinga

[Henrik Böving]

Heh, seems like they updated it to work with Lake just 3 minutes ago, it appears we are being watched silently :eye:

[Marc Huisinga]

It should be compatible with Lake now, I think.

[Marc Huisinga]

It doesn't have autocompletion yet and the final type conversion step isn't type safe. Those are two things that should likely still be improved upon.

[Simon Hudon]

I also have something that I'm playing with. The idea is to annotate your structure declaration and use a deriving command to get the parser out. E.g.:

structure Flags where
  traceCmd :
    CmdLineFlag "-c" (some "--cmd")
    "tracing: print command"
  traceSubst :
    CmdLineFlag "-s" none
    "tracing: print module renaming"
  traceRoot :
    CmdLineFlag "-r" none
    "tracing: print command"
  optValue :
    CmdLineOpt "-t" none Nat
    "tracing: test option parsing"
  dryRun :
    CmdLineFlag "-d" none
    "dry run: calculate parameters but perform no action"

Here is the library: https://github.com/cipher1024/lean4-prog/tree/main/cmd-line-args

It still needs some work and some cleaning up but any feedback would be welcome