automatically get version info

Stream: general

[Asei Inoue]

How to get current date by Lean?

Background

I'm working CLI tool in Lean. I don't want to specify version info manually.
So, I came up with the idea of making the result of running --version be (the Lean version) + (the release date). That way, there should be no need to specify the output of --version manually.

see https://github.com/Seasawher/mdgen/issues/106 for more detail

[Chris Henson]

Are you looking for something like what docs#Std.Time.Timestamp.now or docs#Std.Time.DateTime.now gives?

[Asei Inoue]

Thank you!

[Asei Inoue]

But how can I convert the current time, which is wrapped in the IO monad, into a String…?

[Chris Henson]

@loogle Std.Time.DateTime, String

[loogle]

:search: Std.Time.GenericFormat.format, Std.Time.DateTime.toAscTimeString, and 10 more

[Asei Inoue]

We need to write elaborator to get a String representing current date…?

[Chris Henson]

Oh, I see. From the link above, you want this to go inside the Cli DSL? I've not used that library before, sorry.

[Asei Inoue]

Yes!

[Jon Eugster]

is
let now := (← Std.Time.PlainDate.now) |>.format "uuuu-MM-dd"
what you want? That's run in the IO monad

[Asei Inoue]

@Jon Eugster

Thank you. I will try this:

/-- Get the release date of the project -/
def getReleaseDate : IO String := do
  let date ← Std.Time.PlainDate.now
  return date.format "uuuu-MM-dd"

/-- version message of `mdgen --version` -/
unsafe def versionMsg : String :=
  let dateExcept := unsafeIO getReleaseDate
  let date := match dateExcept with
    | Except.ok date => date
    | Except.error _ => "unknown date"
  s!"{Lean.versionString} (released on {date})"

/-- API definition of `mdgen` command -/
unsafe def mkMdgenCmd : Cmd := `[Cli|
  mdgen VIA runMdgenCmd; [versionMsg]
  "mdgen is a tool to generate .md files from .lean files."

  FLAGS:
    c, count; "Counts the total number of characters in the input Lean files. However, please be aware that the output may not be entirely accurate."
    e, exercise; "Erases parts of Lean code and replaces them with sorry."

  ARGS:
    input_dir : String; "The directory containing the input Lean files."
    output_dir : String; "The directory to write the markdown files."
]

[Eric Wieser]

Usually version dates indicate when the code was changed, not when it was compiled

[Eric Wieser]

Especially since Lean projects are almost always shipped as source

[Asei Inoue]

@Eric Wieser Thanks.

How about this? This code get release date from git.

/-- Get the release date of the project -/
def getReleaseDate : IO String := do
  let out ← IO.Process.output {
    cmd := "git"
    args := #["log", "-1", "--format=%cs"]
  }
  return out.stdout.trimRight

/-- version message of `mdgen --version` -/
unsafe def versionMsg : String :=
  let dateExcept := unsafeIO getReleaseDate
  let date := match dateExcept with
    | Except.ok date => date
    | Except.error _ => "unknown date"
  s!"{Lean.versionString} (released on {date})"

/-- API definition of `mdgen` command -/
unsafe def mkMdgenCmd : Cmd := `[Cli|
  mdgen VIA runMdgenCmd; [versionMsg]
  "mdgen is a tool to generate .md files from .lean files."

  FLAGS:
    c, count; "Counts the total number of characters in the input Lean files. However, please be aware that the output may not be entirely accurate."
    e, exercise; "Erases parts of Lean code and replaces them with sorry."

  ARGS:
    input_dir : String; "The directory containing the input Lean files."
    output_dir : String; "The directory to write the markdown files."
]

[Eric Wieser]

That's a little better, but calling git every time your binary is invoked sounds like a bad idea

[Asei Inoue]

@Eric Wieser

so you mean "getting version info automatically" is bad idea?

[Eric Wieser]

Well, ideally you would only call git when you pass the--version flag, so as not to slow things down

[Eric Wieser]

But yes, doing this automatically seems fishy to me

[Asei Inoue]

ok, I should check version info automatically when developing it?