upstreaming Mathlib.Lean.Json

Stream: lean4

[llllvvuu]

do people think it’s worth upstreaming file#Mathlib/Lean/Json (a pretty small file) and adding the one-liners for UInt64 etc?

[Eric Wieser]

I think the entire Mathlib.Lean folder is "things which should be upstreamed but the author doesn't want to wait 1-2 months before they are available in mathlib".

[Eric Wieser]

Obviously core probably doesn't want everything in there, but I think the Json file should be uncontroversial (modulo bikeshedding the error messages)

[llllvvuu]

somewhat unrelated: out of curiosity, are JSON/XML parsing not intended to be in the stdlib? I was somewhat surprised to see them under Lean and not Init

[Eric Wieser]

I think at one point Init was not allowed to import Lean, and so it would be impossible to write the json% elaborator solely within Init. Maybe that rule has been relaxed now.

[François G. Dorais]

That rule hasn't been relaxed but now there is also Std in between Init and Lean.

[Kim Morrison]

I'm a bit skeptical about running predicates in fromJson?

[Eric Wieser]

Kim Morrison said:

I'm a bit skeptical about running predicates in fromJson?

Is this complaint leveled at the Fin instance, or just the Subtype one?

[Henrik Böving]

Eric Wieser said:

Kim Morrison said:

I'm a bit skeptical about running predicates in fromJson?

Is this complaint leveled at the Fin instance, or just the Subtype one?

And I do think that Fin makes sense as it's a cheap check but Subtype is potentially dangerous as an adversary could make you execute potentially highly expensive computation.

[llllvvuu]

I took a look at Lean/Data/Json/FromToJson and it seems UInt64 is already handled (I didn't notice since the one that I needed was actually UInt32), but it gets serialized as a string, unlike Nat/Int:

import Lean
#eval Lean.toJson (UInt64.size - 1 : Nat)
#eval Lean.toJson (UInt64.size - 1 : Int)
#eval Lean.toJson (0-1 : UInt64)

Now I'm not sure what would be the right thing for Fin (probably still a number like Nat?).

[Notification Bot]

A message was moved from this topic to #lean4 > Importing Lean from Std and Init by Eric Wieser.

[Eric Wieser]

Json serializing as a string sounds wrong to me there

[Eric Wieser]

I understand that the javascript JSON.parse loses precision when parsing uint64s, but really that's the job of the parser to use a better parsing library (like https://www.npmjs.com/package/json-with-bigint).

[Eric Wieser]

Henrik Böving said:

And I do think that Fin makes sense as it's a cheap check but Subtype is potentially dangerous as an adversary could make you execute potentially highly expensive computation.

For instance if your field is {p : Nat // p.Prime}, and your adversary gives you a very large prime?

[Henrik Böving]

Yes