Add and test encapsulation

[lenianiva]

I don't know if we can upload this to pypi yet, because the Lean 4 based executable might not be able to run in a standalone environment.

[RexWzh]

I think we have two main ways to handle this:

1. Pre-building and uploading artifacts to PyPI
   This could work if the builds aren't too large (PyPI limits: single file size to 100 MiB and total project size to 10 GiB). It's the most user-friendly approach - just pip install and go.

2. Building during install or runtime
   This is more flexible. We could either build on first run, or just provide build scripts and let users handle it.

I'd lean towards pre-building - it's simpler for everyone. For the dynamic building approach, we could leverage GitHub Actions to automate the build process and provide better cross-platform support.

[RexWzh]

Regarding your comment about LeanDojo in the article:

Pantograph has several key architectural improvements over LeanDojo. First of all, it is written entirely in Lean 4. This removes the need for external dependencies (such as Docker) and also improves the speed of interaction. Also, some tactics not supported by LeanDojo, such as have, are available in Pantograph. Other tactics, such as conv and calc...

LeanDojo has actually been Docker-free for quite some time. It interact with traced repositories, relying on two Lean scripts (Lean4Repl.lean and ExtractData.lean). The Python package serves merely as a wrapper, similar to PyPantograph.

The tactic support (such as 'have' and 'calc') is indeed a limitation in LeanDojo, and this makes Pantograph more valuable. :)

[lenianiva]

I think we have two main ways to handle this:

1. Pre-building and uploading artifacts to PyPI
   This could work if the builds aren't too large ([PyPI limits](https://peps.python.org/pep-0759/): single file size to 100 MiB and total project size to 10 GiB). It's the most user-friendly approach - just pip install and go.

2. Building during install or runtime
   This is more flexible. We could either build on first run, or just provide build scripts and let users handle it.

I'd lean towards pre-building - it's simpler for everyone. For the dynamic building approach, we could leverage GitHub Actions to automate the build process and provide better cross-platform support.

Can the pre-built Pantograph repl run in an environment with no lake or lean?

[RexWzh]

Can the pre-built Pantograph repl run in an environment with no lake or lean?

I believe not. Perhaps we could adopt the second method - building in .pantograph when the user first uses Pantograph and no cache is found.

Currently, the repository uses git submodules to fetch Lean code, which might take some effort to upload to PyPI.

For immediate development needs, I suggest:

1. Focus on fixing the interaction bugs
2. Set up a CI pipeline for testing in the current setting, example config from repl
3. When the development is ready for release, consider a different approach:
   • Separate the development of lean repl and the python wrapper.
   • Cache builds in $HOME/.pantograph, similar to .elan

This approach could also enable support for multiple versions based on project-specific lean-toolchain requirements.

---

BTW, I get an installation issue when using Conda.

One needs to use pip install -e . or manually copy the pantograph-repl to the environment:

cp PyPantograph/pantograph/pantograph-repl $HOME/miniconda/envs/pantograph/lib/python3.11/site-packages/pantograph

Otherwise, the Python code only works within the PyPantograph folder.

This issue would be resolved with the caching approach.

[lenianiva]

The interaction bugs are fixed and I'm waiting for user feedback to close the issues and merge the PRs into mainline (deadline by the end of this week).

The Lean repl is already in a separate repository, so its separate.

I don't use conda, so I will not be able to help you with conda issues. I think you'll have to work with pip install -e ..

I'll do the housekeeping work after we figure out a stable way to deliver this software to the users.