Pantograph/PyPantograph setup on Windows

Stream: new members

[Nonye Okoma]

Pantograph Github: https://github.com/leanprover/Pantograph
PyPantograph Github: https://github.com/stanford-centaur/PyPantograph?tab=readme-ov-file

I am attempting to setup PyPantograph so that I can extract data (e.g. Expr) from lean to use in Python. Whenever I try to use the Server() function in a python script, I get this message:

"Traceback (most recent call last):
File "C:\Users\xxx\PyPantograph\mylean\test.py", line 3, in <module>
server = Server(project_path="C:/Users/xxx/PyPantograph/Mylean/.lake/build/lib/lean", timeout=30)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "C:\Users\xxx\PyPantograph\pantograph\server.py", line 84, in __init__
self.restart()
File "C:\Users\xxx\PyPantograph\pantograph\utils.py", line 18, in wrapper
return loop.run_until_complete(func(*args, **kwargs))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "C:\Users\xxx\AppData\Local\Programs\Python\Python312\Lib\asyncio\base_events.py", line 687, in run_until_complete
return future.result()
^^^^^^^^^^^^^^^
File "C:\Users\xxx\PyPantograph\pantograph\server.py", line 168, in restart_async
assert ready == "ready.", f"Server failed to emit ready signal: {ready}; This could be caused by Lean version mismatch between the project and Pantograph or insufficient timeout."
^^^^^^^^^^^^^^^^^
AssertionError: Server failed to emit ready signal: ; This could be caused by Lean version mismatch between the project and Pantograph or insufficient timeout."

Does anyone know how to get this working on Windows?

[Evan Wang]

I believe the problem is the path you are pointing towards. It is supposed to be pointing towards the Lean repository, not the build of it in .lake/.

I've also heard that Pantograph has had some struggles with Windows in the past, I generally work on WSL. For Lean stuff in general, its just been less of a hassle.

[Nonye Okoma]

I just used the WSL setup that you recommended and it worked. Much appreciated.