lean4
lean4 copied to clipboard
RFC: `lake run --help` could explain what a script is
It would be nice if reading lake run --help was sufficient to understand how to write a script, and where to put one. It would be fine if it linked to such an explanation rather than including it inline.
For usability purposes, it might be best if someone other than me updated the help text and PR'd it. My level of familiarity may be disadvantageous in determine what the proper blurb here is. I would be happy to answer any questions in the process.