json float format should have extra .0 if it's an integer

[YangKeao]

Enhancement

Printing json 1.0 will get 1, which is not expected. It should print 1.0.

[YangKeao]

There are three different implementations inside:

MySQL: Use a customized function to serialize float number
TiDB: Use a wrapper function around the standard libraries to format float
TiKV: Use ryu to serialize float.

They have different behaviors for the following situation:

1. The choice between scientific notation and normal notation is different (though I haven't constructed an example of the difference 🤦‍♂️ ). (For TiDB, it's quite simple: if it's ge than 1e21, or less than 1e-6, it's represented in scientific notation. For TiKV, it's more complicated, see https://github.com/dtolnay/ryu/blob/master/src/f2s.rs#L127).
2. The positive exponent part doesn't include "+" in TiKV and MySQL, but do include "+" in TiDB
3. The tailing .0 is added for integer in TiKV and MySQL, but not in TiDB.

For the 2 and 3, we could align the behavior of TiKV, MySQL and TiDB by adding some strategies in TiDB, but for the 1 problem, I haven't thought out a good idea.

What's your opinion? @xiongjiwei

[xiongjiwei]

I think it is ok. Although they have different represent, they still have the same value, we just need to make sure the type is float