search

leanprover-community / lean-client-python

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

Support Lean 3.15.0 (including widgets) #14

Open jasonrute opened 4 years ago

jasonrute commented 4 years ago

The newest version of the lean server now has widgets. Our current code breaks. I think the refactor proposed in #6 (or just adding to the PR #5) could make the lean client more future proof.

jasonrute commented 4 years ago

Specifically, the problems start in Lean 3.15.0. Here is an error when doing an info command:

Traceback (most recent call last):
  File "/tmp/mathlib/scripts/find_and_replace.py", line 152, in <module>
    trio.run(main, path, old, new)
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/trio/_core/_run.py", line 1718, in run
    raise runner.main_task_outcome.error
  File "/tmp/mathlib/scripts/find_and_replace.py", line 105, in main
    nursery.cancel_scope.cancel()
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/trio/_core/_run.py", line 723, in __aexit__
    raise combined_error_from_nursery
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/lean_client/trio_server.py", line 73, in receiver
    resp = parse_response(line.decode())
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/lean_client/commands.py", line 386, in parse_response
    return InfoResponse.from_dict(dic)
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/lean_client/commands.py", line 206, in from_dict
    dic['record'] = InfoRecord.from_dict(dic.pop('record'))
  File "/tmp/mathlib/lean-python-env/lib/python3.7/site-packages/lean_client/commands.py", line 197, in from_dict
    return cls(**dic)
TypeError: __init__() got an unexpected keyword argument 'widget'

You can tell widget is now a new key returned in the dictionary.

PatrickMassot commented 4 years ago

It would be nice if the Lean core development could document that kind of changes. Did you see anything there?

jasonrute commented 4 years ago

I'm not sure what you mean by "lean core development" and "there". Are you talking about the lean repo? A thread/stream on Zulip? Somewhere else?

bryangingechen commented 4 years ago

The relevant PR is https://github.com/leanprover-community/lean/pull/258. I think you can ping @EdAyers if you have any questions.

EdAyers commented 4 years ago

Hi, sorry about this. you can add ‘—no-widgets’ or -W to not return any widget info from the server.

jasonrute commented 4 years ago

@EdAyers I think we want to support widgets (They are a cool feature!), but maybe in the future, we can get a heads-up here (in the form of an issue or a PR) if the shape of the data from the lean server is going to change. Thanks!

jasonrute commented 4 years ago

Also, thanks for the flag info! That would be good to know for any apps currently using the server (like my refactor app which I gave Johan).

PatrickMassot commented 4 years ago

I meant that the Lean server mode is globally undocumented, and it would be nice if new cool features like this widget thing could change that undocumenting tradition.