Lean Continue Backend Service

=================================

Lean Continue aims to integrate Lean Copilot's functionalities (suggest_tactics, search_proof, select_premises) with Continue. Make the Lean Copilot user experience more friendly and seamless.

demo.mov

Requirements

Please follow the steps listed below to install the requirements.

pip install -r requirements.txt

Running the Server

uvicorn server:app --port 23337

Install Lean Continue Frontend

With the running lean copilot service, you can then use Continue to interact with Lean Copilot.

Requirements

• Download and install VS Code.

Steps

1. Download the Lean Continue extension file: https://drive.google.com/file/d/1Ic79-UsSybzC_eGs7pUd3DKDs8oVi6dg/view?usp=sharing

2. Install the extensions by "Install from VSIX" in VScode extensions bar.

3. Open Lean Continue.

4. In left bar of Continue, Select Add Chat model and enter the address of your Lean Copilot HTTP Service, like http://127.0.0.1:23337/generate. Note that here you need to add /generate after your address to get the generation service.

5. Finally, you can enjoy the user friendly proof automation, e.g., suggesting tactics/premises and searching for proofs in Continue.