Commit 2025-01-07 21:11 0e673d61

fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) Hopefully, this fixes the bench_summary bot. You can see the error that the bot reports here, specifically it says

<stdin>:248:81: error: failed to synthesize
  OfNat String 12648073160
numerals are polymorphic in Lean, but the numeral `12648073160` cannot be used in a context where the expected type is
  String
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The issue is that the (lean) script takes the jobID as a String, since it wants to print the jobID url. However, due to quotation handling, the script receives a numeric literal, since the double quotes get lost in translation. If instead we ask Lean to do the conversion of a natural number to a string internally, everything should work.