leanprover-community / lean-client-python

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

Refactor commands API #19

Closed jasonrute closed 3 years ago

jasonrute commented 3 years ago

Sorry. I did this work a long time ago but never made a PR. ~I think its ready to go, but I'll look it over again tomorrow and add a better description of the work.~

Update: This is now ready to go

The main point of this PR is as follows:

Still TO DO:

Do do in another PR:

jasonrute commented 3 years ago

Ok. This is ready to go. What do you think @PatrickMassot ?

jasonrute commented 3 years ago

@Julian I'd be interested in your thoughts on this as well.

Julian commented 3 years ago

Support widgets (issue #18). I added no code in support of widgets. It is a terribly complex interface which makes me question our decision to hard code the lean interface (instead of just leaving it as JSON).

I mentioned I had evil ideas somewhere -- said evil ideas are I'm somewhat confident I can make this just parse the typescript interfaces into Python classes rather than reimplementing them which would super simplify things I suspect, (and do so in a way that benefits the Python ecosystem beyond this project). I have a POC of parsing Typescript interfaces but haven't had time to turn it into a real thing the past few weeks. But.. at some point I think I can do that. So my thoughts if any on that track are probably it's worth doing the bare minimum to churn along here and then probably try the sledgehammering :).

Will have a look at the rest at some point, probably after this weekend though since I keep procrastinating something else I should be working on.

jasonrute commented 3 years ago

I can make this just parse the typescript interfaces into Python classes rather than reimplementing them which would super simplify things I suspect

I admit I don't see the benefit of this @Julian. If we implement the classes, then we have (1) documentation, (2) a static type system that we can use mypy, PyCharm, or VSCode to inspect and catch errors, as well as (3) in editor tab completion. If we don't want any of that, then we can just use Python's usual approach of converting JSON into dicts, lists, floats, ints, bools, etc. One tool that sort of bridges those divides is ProtoBufs, but that requires the interface to be documented somewhere in a .proto file and then the python file is automatically created. (But I don't think the server protocol is compatible with ProtoBuffs, or is it documented in a similar way.)

Julian commented 3 years ago

Fair enough obviously I'll try and convince you before doing anything. And yeah if you're after the static typing tooling then it's definitely a tradeoff (the tradeoff being these kinds of issues with Widget -- where the server is speaking a different protocol than you are, and you get to now reimplement a chunk of annoying objects). But yeah it's not terribly important either. Will worry about reviewing this as-is first certainly.

PatrickMassot commented 3 years ago

Thanks a lot for all your work. Let's merge this, we can still improve stuff later.