[WIP] subprocess version of python/lean communication

[seanmcl]

Had to comment out the assert statements which aren't supported yet, but this makes the getting-started example go through

 $ interop/test.sh
 json file: /var/folders/hz/hgkdl8pj5fg_zlm2qh8x8fy40000gr/T/tmp6iaqtmi8.json
   4 = nki.language.load(%a_input<float64:128,512>)
   5 = nki.language.load(%b_input<float64:128,512>)
   6 = nki.language.add(4,5)
   7 = nki.language.store(%c_output<float64:128,512>,value=6)

Just an idea.

[govereau]

In general, I think this approach better, it is easier to maintain. I am not entirely convinced that we won't need to integrate more closely with python in the future, but we can cross that bridge if we come to it.

[govereau]

So, technically you are not writing KLR.json, right?
Do you just need to derive Lean.ToJson on the KLR types and call toJson?

[seanmcl]

Yeah, I just copied the text format back to Python for the poc. I'll call toJson.

[seanmcl]

Now the example test writes

$ python3 test/test_examples.py
[{"assign":
  {"x": "4",
   "e":
   {"call":
    {"kwargs": [],
     "f": {"var": {"x": "nki.language.load"}},
     "args":
     [{"tensor":
       {"t":
        {"shape": [128, 512], "name": "a_input", "dtype": "float64"}}}]}}}},
 {"assign":
  {"x": "5",
   "e":
   {"call":
    {"kwargs": [],
     "f": {"var": {"x": "nki.language.load"}},
     "args":
     [{"tensor":
       {"t":
        {"shape": [128, 512], "name": "b_input", "dtype": "float64"}}}]}}}},
 {"assign":
  {"x": "6",
   "e":
   {"call":
    {"kwargs": [],
     "f": {"var": {"x": "nki.language.add"}},
     "args": [{"var": {"x": "4"}}, {"var": {"x": "5"}}]}}}},
 {"assign":
  {"x": "7",
   "e":
   {"call":
    {"kwargs": [["value", {"var": {"x": "6"}}]],
     "f": {"var": {"x": "nki.language.store"}},
     "args":
     [{"tensor":
       {"t":
        {"shape": [128, 512], "name": "c_output", "dtype": "float64"}}}]}}}}]

Good enough for now?

[govereau]

Seems ok. I am working out the BIR output now, it will be similar.