Scientific Representation for Float

Stream: lean4

[Alfredo Moreira-Rosa]

By default Repr represent Float without without Scientific notation.
This is annoying when Float are really small for example, because Repr will show them as 0.000000.
So is there an option to change the default Repr ?
If not would a PR be acceptable to change the Repr to use Scientific notation when the number is too small or too big ?

[Alfredo Moreira-Rosa]

It was asked here also :
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.22.25.2E5g.22.20.25.20x.20for.20Float/with/418168531

[Arthur Paulino]

IIRC you can set priorities for instances. Something along the lines of

instance (priority := high) : Repr Float where
  ...

[Alfredo Moreira-Rosa]

Yes, i did that in custom code. But i was thinking about adding it natively. And wanted to know if such a change would be accepted

[Robin Arnez]

Funnily enough, we'd probably get scientific notation if we used C++26 (we use std::to_string)
https://en.cppreference.com/w/cpp/string/basic_string/to_string

[Arthur Paulino]

ecyrbe said:

Yes, i did that in custom code. But i was thinking about adding it natively. And wanted to know if such a change would be accepted

Ah, I think that's sensible.
This is what Python 3.10.12 shows

>>> 0.000000000000000003
3e-18

And this is what Node 20.5.1 shows

> 0.000000000000000003
3e-18

And Rust (toolchain 1.88) shows the exact same thing.

[Alfredo Moreira-Rosa]

Robin Arnez said:

Funnily enough, we'd probably get scientific notation if we used C++26 (we use std::to_string)
https://en.cppreference.com/w/cpp/string/basic_string/to_string

So if we don't want to target c++26, maybe a PR to use c++20 using std::format instead would be ok ?

[Alfredo Moreira-Rosa]

so changing this :

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::to_string(a));

into this :

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));
}

[Alfredo Moreira-Rosa]

I created an RFC here : https://github.com/leanprover/lean4/issues/10349

[Alfredo Moreira-Rosa]

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

[Alfredo Moreira-Rosa]

The configuration to at least switch to CLang 17 is on the Nix configuration here :
https://github.com/leanprover/lean4/blob/master/flake.nix

And we would need to change this line :

      llvmPackages = pkgs.llvmPackages_15;

into this :

      llvmPackages = pkgs.llvmPackages_17;

And add the flag on CMakeList.txt to use std:c++20
Not sure how of a breaking change it is to update Lean4 C++ toolset.

@Sebastian Ullrich is it complicated ?

[Jakub Nowak]

This works even with C++11

#include <iostream>
#include <sstream>
#include <string>

std::string double_to_string(double a)
{
    std::ostringstream oss;
    oss << a;
    return oss.str();
}

int main()
{
    std::cout << double_to_string(0.01) << std::endl;
    std::cout << double_to_string(0.00000000000000000000001) << std::endl;
}

[Robin Arnez]

Right, the std::cout option described in the docs. I think the main difference to std::format is that it is inprecise; but so is the current version so I guess that would still be some improvement.

[Jakub Nowak]

There's std::to_chars in C++17 if you want shortest unique representation. But I think Lean is build with C++14?