-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support Lean 3.15.0 (including widgets) #14
Comments
Specifically, the problems start in Lean 3.15.0. Here is an error when doing an info command:
You can tell |
It would be nice if the Lean core development could document that kind of changes. Did you see anything there? |
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? |
The relevant PR is leanprover-community/lean#258. I think you can ping @EdAyers if you have any questions. |
Hi, sorry about this. you can add ‘—no-widgets’ or -W to not return any widget info from the server. |
@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! |
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). |
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. |
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.
The text was updated successfully, but these errors were encountered: