Json ser-deser

Stream: lean4

[Henrik Böving]

I'm currently working the autogenerated FromJson, ToJson instances to dump some info to a JSON file and read it in in another part of doc-gen, the input can be parsed as JSON just fine but the autogenerated ToJson instance gives me some "String expected" error so it apparently doesn't like the format the ToJson generated? At least when viewing the file I can validate that it has the correct format:

structure JsonDeclaration where
  name : String
  doc : String
  docLink : String
  sourceLink : String
  deriving FromJson, ToJson

structure JsonInstance where
  name : String
  className : String
  deriving FromJson, ToJson

structure JsonModule where
  name : String
  declarations : List JsonDeclaration
  instances : Array JsonInstance
  imports : Array String
  deriving FromJson, ToJson

(The List and Array stuff are there for a reason)
On an value of JsonModule toJson produces a file like this:

{
  "name":"Init.NotationExtra",
  "instances":[{"name":"Lean.instForInLoopUnit","className":"ForIn"}],
  "imports":["Init.Meta","Init.Data.Array.Subarray","Init.Data.ToString"],
  "declarations":[
    {"sourceLink":"https://github.com/leanprover/lean4/blob/3846dd60fd5bbb7901b432066234037c35b872a0/src/Init/NotationExtra.lean#L275-L275","name":"Lean.«term_Matches_|»","docLink":"./Init/NotationExtra.html#Lean.«term_Matches_|»","doc":""},
  ......
   ]
}

and the fromJson? throws its "String expected" error.

How would I go about debugging this?

[Henrik Böving]

Minimizing further it doesn't even like:

{
  "name":"Init.NotationExtra",
  "instances":[],
  "imports":[],
  "declarations":[]
}

[Gabriel Ebner]

How are you calling the JSON parser?

[Henrik Böving]

#eval show IO _ from do
  let foo ← IO.FS.readFile (System.FilePath.mk "."/ "DocGen4" / "Output" / "mytest.json")
  IO.println foo
  match (fromJson? foo : Except _ JsonModule) with
  | .ok foo => pure foo.name
  | .error err => pure err

is my test case right now

[Gabriel Ebner]

I fear there might be a certain coercion from String to Json that you're using here.

[Eric Wieser]

On a tangent: presumably at some point I should bring docs#json_serializable in line with docs4#ToJson and docs4#FromJson?

[Gabriel Ebner]

Or maybe the other way around? I never liked the separation of FromJson and ToJson.

[Henrik Böving]

Gabriel Ebner said:

I fear there might be a certain coercion from String to Json that you're using here.

Can you elaborate?

[Eric Wieser]

docs#polyrith.poly.non_null_json_serializable has a dummy function for serialization, so I think the split might make sense

[Eric Wieser]

Either that, or we should have toJson : α → except String Lean.Json to permit sometimes-serializable objects

[Gabriel Ebner]

Can you elaborate?

fromJson? takes a Json argument. In your example, foo is a string. So fromJson? foo means fromJson? (.str foo).

[Henrik Böving]

ohhhhhh

[Henrik Böving]

so fromJson? (Json.parse foo) instead

[Gabriel Ebner]

docs#polyrith.poly.non_null_json_serializable has a dummy function for serialization, so I think the split might make sense

Ideally sage would just return JSON in the schema expected by deriving JsonSerializable for Poly.

[Henrik Böving]

Alright working now, thanks :thumbs_up:

[Eric Wieser]

Gabriel Ebner said:

docs#polyrith.poly.non_null_json_serializable has a dummy function for serialization, so I think the split might make sense

Ideally sage would just return JSON in the schema expected by deriving JsonSerializable for Poly.

In this case we send send the polys to sage in a completely different format to the format we receive them; which is obviously messy.