Python package #5
Conversation
|
Currently, we require users to build the package from source from within this repository. Once we get the compiled version of the repl working, the python package should be installable with only |
|
|
||
| # python gitignore | ||
| # Byte-compiled / optimized / DLL files | ||
| __pycache__/ | ||
| *.py[cod] | ||
| *$py.class |
There was a problem hiding this comment.
Could we not add the kitchen sink, but just what is needed?
| Running Lean programs that `import Mathlib` is a common use case. To enable `mathlib4` imports, simply add the following to `lakefile.lean` and run `lake exe cache get` before running `lake build`. | ||
| ``` | ||
| require mathlib from git | ||
| "https://github.com/leanprover-community/mathlib4.git" | ||
| ``` |
There was a problem hiding this comment.
People shouldn't be adding a mathlib dependency to the lakefile of this project. Perhaps clarify that you'll need your own lakefile?
| print(output) | ||
| return json.loads(output) | ||
| except pexpect.exceptions.TIMEOUT: | ||
| raise pexpect.exceptions.TIMEOUT |
There was a problem hiding this comment.
What's the point in this except? It looks like all it does is make the traceback noisier
| self.proc.sendline() | ||
| self.proc.expect_exact("\r\n") | ||
| try: | ||
| index = self.proc.expect('env": \d+\}', timeout=20) |
There was a problem hiding this comment.
Can you expect the whole line here and parse it as json, rather than parsing using regex?
There was a problem hiding this comment.
It can't because there are multiline outputs.
There seems to be no guarantee in the Lean code that env will appear at the last, so this is not robust.
Per my test of repl and this comment in the code, repl is using \r\n\r\n as delimiters for requests/responses, just like in HTTP protocol, this is probably the only way to expect here, except to use a loop to expect more lines until the response becomes a valid JSON, which would wastes many JSON parse attempts, or we have to deal with these using fragile regexes.
My implementation inspired by this PR but expecting \r\n\r\n protocol is here, notably, it turns off echo so there is less expecting.
For the stability of parsing repl's output, I hope this \r\n\r\n protocol could be explicitly documented.
| self.proc.sendline(command) | ||
| self.proc.expect_exact(command + "\r\n") | ||
| self.proc.sendline() | ||
| self.proc.expect_exact("\r\n") |
There was a problem hiding this comment.
Does this work on unix? I wouldn't expect there to be an \r there
There was a problem hiding this comment.
This works on my ubuntu system.
There was a problem hiding this comment.
I believe the \r\n is part of JSON-RPC which is the basis for LSP
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Thanks for the reviews. I see that since I opened this PR, the bug that prevented the repl from compiling was fixed. Therefore I'm going to convert this PR back to a draft and work on a version of the python package that installs a pre-compiled binary of the repl. |
| if env: | ||
| command = ( | ||
| json.dumps(dict(cmd=code, env=env)) | ||
| ) # [1:-1] removes single quotes | ||
| else: | ||
| command = ( | ||
| '{ "cmd" : "' + repr(code)[1:-1] + '" }' | ||
| ) # [1:-1] removes single quotes |
There was a problem hiding this comment.
| if env: | |
| command = ( | |
| json.dumps(dict(cmd=code, env=env)) | |
| ) # [1:-1] removes single quotes | |
| else: | |
| command = ( | |
| '{ "cmd" : "' + repr(code)[1:-1] + '" }' | |
| ) # [1:-1] removes single quotes | |
| data = dict(cmd=code) | |
| if env: | |
| data.update(env=env) | |
| command = json.dump(data) |
Adds python interface via a package called
pylean. SeeREADME.mdfor usage instructions. Unit tests inpylean/tests.