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.

[RexWzh]

A solution for separating the Pypantograph and Pantograph

Instead of combining the two projects using submodules, we can implement a more modular and user-friendly solution.

Here’s an example of how to use it:

1. Install Pypantograph:

   pip install pantograph  # Installs the package and gives some helpful CLI tools

2. Check Available Versions:

   p2g list  # Lists stable Pantograph versions, e.g., 4.12.0, 4.14.0

3. Download and Build a Specific Version:

   p2g install 4.12.0  # Downloads and builds version 4.12.0 into a cache at ~/.pantograph

When working in Python, you could set up the server like this:

• Point to a Specific Directory:

  server = Server(project_path, ..., cwd='your-directory')  # Use any directory where Pantograph is set up

• Use a Cached Version by Tag or Commit:

  server = Server(project_path, ..., tag_or_commit_hash='4.12.0')  # Loads the version from ~/.pantograph/

[RexWzh]

Moreover, I think non-essential dependencies, such as torch, should be removed from pyproject.toml to keep it lightweight. This could reduce the time it takes to run poetry install during local development or in GitHub CI/CD pipelines.

pyproject.toml#L30

As for LLM integration, I think supporting the OpenAI-style API should be sufficient since most other LLMs can either be loaded in (e.g. using vllm) or adapted to this format(e.g. lite-llm, one-api).

It takes a long time when I try to merge the latest commit and rebuild the dependencies.

Let me know your thoughts.

[lenianiva]

Moreover, I think non-essential dependencies, such as torch, should be removed from pyproject.toml to keep it lightweight. This could reduce the time it takes to run poetry install during local development or in GitHub CI/CD pipelines.

pyproject.toml#L30

As for LLM integration, I think supporting the OpenAI-style API should be sufficient since most other LLMs can either be loaded in (e.g. using vllm) or adapted to this format(e.g. lite-llm, one-api).

It takes a long time when I try to merge the latest commit and rebuild the dependencies.

Let me know your thoughts.

All the non-essential dependencies have been removed. If there is any future MCP integration, they should stay in another repo.