json.parse "-1" = some (json.of_int 4294967295)

Stream: general

[Eric Wieser]

This looks like a bug to me

run_cmd do
  j@(json.of_int i) ← json.parse "-1",
  tactic.trace i,            -- `4294967295`
  tactic.trace j.to_format,  -- `4294967295`
  tactic.trace j.unparse     -- `-1`

-- succeeds
run_cmd guard (json.parse "4294967295" = json.parse "-1")

at least docs#json.parse and docs#json.unparse round trip, but they don't decode to the expected result

[Jason Rute]

I thought @Edward Ayers added the json stuff to Lean 3, so maybe he has some thoughts on this.

[Eric Wieser]

I haven't really looked in detail at the lean3 source yet, but would be surprised if nothing similar has been noticed before

[Edward Ayers]

Yep definitely a bug

[Edward Ayers]

Fix here: https://github.com/leanprover-community/lean/pull/740

[Eric Wieser]

What does 4294967295 now parse as?