RFC: Float Repr should use Scientific notation when too small or too big

[ecyrbe]

Proposal

Clear and detailed description of the proposal. Consider the following questions:

• User Experience: How does this feature improve the user experience? Today small Floats (like 1e-15) are shown as 0.00000 and big one with too much decimals. This don't match usual behaviour of printing Floats in other programming languages.

• Beneficiaries: Which Lean users and projects benefit most from this feature/change? It's a daily life improvement for scientific computing using Floats

• Maintainability: Will this change streamline code maintenance or simplify its structure? No change in maintainability of the code

Community Feedback

This was discussed here : #lean4 > Scientific Representation for Float

Impact

The change is in this c++ runtime code

Options :

• switch to c++26 (behaviour of std::to_string will match std::format, see cpp docs
• change implementation to use std::format directly :

#include <format>
...

extern "C" LEAN_EXPORT lean_obj_res lean_float_to_string(double a) {
    if (isnan(a))
        // override NaN because we don't want NaNs to be distinguishable
        // because the sign bit / payload bits can be architecture-dependent
        return mk_ascii_string_unchecked("NaN");
    else
        return mk_ascii_string_unchecked(std::format("{}", a));
}

[ecyrbe]

After some tests, it seems we are using CLang 15, to be able to use c++20, we would need to switch to at least CLang 17 and activate std:c++20

[Kha]

RFC accepted!