RFC: Enhanced APIs for Float parsing and formatting

Proposal

One of the basic needs for writing a program is parsing and formatting floating-point numbers. Unfortunately, Lean is currently very lacking in this area IMO:

• Parsing: The closest we have is OfScientific. We don't have any function that parses a String directly to a Float.
• Formatting: The only thing we have is ToString, which just calls C++ std::format, which in turn gives a string with default precision. We cannot choose between fixed/scientific notation, and we cannot specify a custom precision. Batteries.Float.toStringFull exists, but it is still a hassle to manipulate its output further to get the desired output.

Basic proposal:

• Implement String.toFloat? and String.toFloat! which are like String.toNat? and String.toNat! but for Float
• Implement, say, Float.to{Fixed|Scientific} (prec := some default value). There may be more detailed formatting needs such as e vs. E, explicit vs. implicit + in exponents; whether and how to support these may be discussed further

Direct benefits:

• These interfaces make life much easier when writing various application programs
• We could simplify a part of Lean infrastructure, e.g. float parsers/formatters for JSON and TOML
  • For parsing, I believe the places where a number token can appear are limited in both formats, so we can get away with something like passing a [0-9eE.+-]+ token to the toFloat? function.

Maintainability concerns:

• If we stick to simple pure-Lean implementation, probably not so much?
• If we care about performance and/or correctness, algorithms such as https://github.com/ulfjack/ryu may be used, but these are significantly more complex to re-implement in Lean
  • Vendoring ryu's C implementation could be an option.

Community Feedback

I posted the idea of using ryu for this functionality on this Zulip thread but didn't get any response.

Start by reviewing the existing String.toNat? and String.toNat! APIs, along with Batteries.Float.toStringFull, to understand the proposed parsing and formatting interfaces. Clarify supported notation, precision, exponent syntax, and implementation strategy before determining whether the proposal is complete.