plan for `data.json`?

Stream: mathlib4

[Siddhartha Gadgil]

I would guess that instead of defining exceptional and json_serializablethe plan is to use FromJson and ToJson from the lean core?

• Is that correct?
• If so would it be useful to try to make this kind of port (or better to leave this for the core developers to put in Std say)?
• If yes to the above, would it be better to define a single FromToJson class including both and "export" instances to the separate classes or to make pairs of instances while porting?

[Eric Wieser]

I think probably the thing to do is forward-port the missing features from mathlib3 to lean4, rather than do a direct port

[Eric Wieser]

I wrote docs#json_serializable before I was aware that Lean4 had an implementation already

[Eric Wieser]

Backporting to Lean3 would also be quite reasonable

[Eric Wieser]

I don't understand your comment about exceptional; isn't docs#exceptional just docs4#Except ?

[Siddhartha Gadgil]

Eric Wieser said:

I don't understand your comment about exceptional; isn't docs#exceptional just docs4#Except ?

mathlib3port ported exceptionalto a new monad I believe, so in that sense it is not docs4#Except. But I assumed it is meant to be as you say.

[Eric Wieser]

Ah I see, docs4#Lean.FromJson only allows string error messages, not format!"" ones

[Eric Wieser]

So exceptional X in Lean 3 is Except (Lean.Options → Std.Format) X in Lean 4