Rounding of large numbers inconsistent with google/jsonnet

[lihaoyi]

Input: 738529527931269425

• google/jsonnet output: 738529527931269400 (according to https://jsonnet.org/)

  • equivalent to Javascript's parseFloat("738529527931269425")

• databricks/sjsonnet output: 738529527931269376

  • equivalent to Java's (long)java.lang.Double.parseDouble("738529527931269425"), or BigInt(parseFloat("738529527931269425"))

It seems this is mostly an issue in the pretty-printing of floats: JS rounds a bit more than Java does, but in the end both are valid representations for the same double, and are bit-for-bit-identical and are == to each other on both Java and JS.

databricks/sjsonnet is meant to be identical to google/jsonnet, so even if this is an edge case we should probably follow suit

Initially reported in com-lihaoyi/upickle#522