LeanSearch-v2/pyproject.toml at main · frenzymath/LeanSearch-v2 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
[project]
name = "leansearchv2"
version = "0.1.0"
description = "Global premise retrieval for Lean 4 theorem proving."
readme = "README.md"
requires-python = ">=3.11"
license = { file = "LICENSE" }
dependencies = [
    "fastapi>=0.110",
    "uvicorn>=0.29",
    "pydantic>=2.5",
    "python-dotenv>=1.0",
    "pyyaml>=6.0",
    "numpy>=1.26",
    "torch>=2.2",
    "sentence-transformers>=3.0",
    "transformers>=4.51",
    "httpx>=0.27",
    "openai>=1.40",
    "tqdm>=4.66",
    "jinja2>=3.1",
]

[project.optional-dependencies]
# cuVS / RAPIDS — install via the matching CUDA wheel index, e.g.
#   pip install -e ".[cuvs]" --extra-index-url https://pypi.nvidia.com
cuvs = [
    "cuvs-cu12>=25.12",
    "cupy-cuda12x>=13.6",
]
# Lean 4 REPL via lean-interact (only needed for the prove task; requires
# elan/lake on PATH). Install with `pip install -e ".[lean]"`.
lean = [
    "lean-interact>=0.5",
]

[build-system]
requires = ["setuptools>=68", "wheel"]
build-backend = "setuptools.build_meta"

[tool.setuptools.packages.find]
where = ["src"]

[tool.setuptools.package-data]
"leansearchv2.corpus" = ["templates/*.j2"]