diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml index 17071c7..11c78bb 100644 --- a/.github/workflows/weekly-index.yml +++ b/.github/workflows/weekly-index.yml @@ -14,6 +14,9 @@ jobs: JIXIA_REPO: https://github.com/frenzymath/jixia MODULE_NAMES: Physlib DRY_RUN: 'false' + # Each jixia worker loads ~2-3 GB of Mathlib; cap concurrency so the + # runner (16 GB) doesn't get OOM-killed during the load step. + JIXIA_MAX_WORKERS: '2' CHROMA_PATH: chroma CONNECTION_STRING: ${{ secrets.DATABASE_URL }} GEMINI_API_KEY: ${{ secrets.GEMINI_API_KEY }} diff --git a/database/jixia_db.py b/database/jixia_db.py index f57e4f6..1601fd5 100644 --- a/database/jixia_db.py +++ b/database/jixia_db.py @@ -176,12 +176,18 @@ def topological_sort(): with conn.cursor() as cursor: lean_sysroot = Path(os.environ["LEAN_SYSROOT"]) lean_src = lean_sysroot / "src" / "lean" + # Each jixia worker loads the full Mathlib environment (~2-3 GB), so the + # default thread count (CPUs + 4) can exhaust memory and get the process + # OOM-killed. Cap it via JIXIA_MAX_WORKERS in memory-constrained CI. + max_workers_env = os.environ.get("JIXIA_MAX_WORKERS") + max_workers = int(max_workers_env) if max_workers_env else None all_modules = [] for d in project.root, lean_src: results = project.batch_run_jixia( base_dir=d, prefixes=prefixes, plugins=["module", "declaration", "symbol"], + max_workers=max_workers, ) modules = [r[0] for r in results] load_module(modules, d)