Add LeanDojo test and bump external_api toolchain

.github/workflows/pytest.yml

@@ -0,0 +1,55 @@
+name: Pytest
+
+on:
+  push:
+    branches: ["*"]
+  pull_request:
+    branches: ["*"]
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        python-version: ["3.11"]
+    name: run pytest (Python ${{ matrix.python-version }})
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v4
+        with:
+          version: "latest"
+
+      - name: Set up Python ${{ matrix.python-version }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python-version }}
+
+      - name: Create virtual environment
+        run: |
+          uv venv
+
+      - name: Set up elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Install Pantograph
+        run: |
+          uv pip install git+https://github.com/stanford-centaur/PyPantograph
+
+      - name: Install project with dev dependencies
+        run: |
+          uv pip install -e ".[dev]"
+
+      - name: Run pytest
+        env:
+          GITHUB_ACCESS_TOKEN: ${{ secrets.GITHUB_ACCESS_TOKEN }}
+        run: |
+            source .venv/bin/activate
+            pytest -vvv
+

lean_dojo_v2/external_api/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0-rc3
+leanprover/lean4:v4.24.0

lean_dojo_v2/external_api/python/external_models/__init__.py

@@ -1,6 +1 @@
-# from .claude_runner import ClaudeRunner
-# from .gemini_runner import GeminiRunner
 from .hf_runner import HFTacticGenerator
-
-# from .oai_runner import OpenAIRunner
-# from .vllm_runner import VLLMTacticGenerator

lean_dojo_v2/external_api/python/server.py

@@ -4,29 +4,14 @@
 import torch
 from external_models import *
 from fastapi import FastAPI, HTTPException
-from loguru import logger
 from models import *
 from pydantic import BaseModel
 
 app = FastAPI()
 
 models = {
-    "kimina": VLLMTacticGenerator(
-        model="AI-MO/Kimina-Prover-Preview-Distill-7B",
-        tensor_parallel_size=1,
-        temperature=0.6,
-        max_tokens=1024,
-        top_p=0.9,
-        length_penalty=0,
-        n=4,
-        do_sample=True,
-        output_scores=True,
-        output_logits=False,
-        return_dict_in_generate=True,
-        device="auto",
-    ),
     "deepseek": HFTacticGenerator(
-        model="deepseek-ai/DeepSeek-Prover-V2-7B",
+        model="deepseek-ai/DeepSeek-Prover-V2-671B:novita",
         temperature=0.6,
         max_new_tokens=256,
         top_p=0.9,