Add Widget. #18
Add Widget. #18
Conversation
Closes: #14 This seems to be present in lean v3.23.0, and without it, examples/trio_server.py doesn't run here.
|
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. |
|
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". |
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.