search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Add Widget. #18

Closed Julian closed 1 year ago

Julian commented 3 years ago

This seems to be present in lean v3.23.0, and without it, examples/trio_server.py doesn't run here.

(After this and #17, #16 runs for me.)

I haven't read https://github.com/leanprover-community/lean/blob/master/doc/widget_server.md carefully to be honest, I was just trying to see the example work so far, but this seems correct enough to as I say get it working. I didn't see #14 either until after I put this in, but I guess this closes it.

jasonrute commented 3 years ago

Hi Julian! First, thank you for your interest in this project. I'm also sorry because I started fixing all this stuff a while ago. I think I even got it done, but then didn't follow through with a PR. I just made a PR #19. In particular, based on Gabriel's advice it doesn't break if new a field (like widgets) is added to the JSON. However, I didn't actually implement widgets which has a complicated interface. If you are interested in taking that task on, let us know.

Julian commented 3 years ago

All good! I did see some room to do something like that, was just trying to do the minimum possible, but certainly seems like you've got more there.

I was about to send a PR to turn CI on as well, hopefully that makes sense.

But yeah happy to close this one and go with yours?

As for what I'm interested in... I am poking at this essentially because I want to see if it'll help me implement some fancier goal state things without too much effort. So, I'm not sure to be honest how much time I want to pour into this specifically, it kind of depends how distracted I get from all the other things :D. That's probably a long "maybe".