Index #25
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Weekly Index | |
| on: | |
| schedule: | |
| - cron: '0 3 * * 1' # Every Monday at 03:00 UTC | |
| workflow_dispatch: | |
| jobs: | |
| index: | |
| runs-on: ubuntu-latest | |
| env: | |
| PHYSLIB_REPO: https://github.com/leanprover-community/physlib | |
| 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 }} | |
| GEMINI_MODEL: ${{ vars.GEMINI_MODEL || 'gemini-3-flash-preview' }} | |
| GEMINI_FAST_MODEL: ${{ vars.GEMINI_FAST_MODEL || 'gemini-3-flash-preview' }} | |
| GEMINI_EMBEDDING_MODEL: ${{ vars.GEMINI_EMBEDDING_MODEL || 'gemini-embedding-2-preview' }} | |
| steps: | |
| - name: Checkout main | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: main | |
| - name: Install Heroku CLI | |
| run: curl https://cli-assets.heroku.com/install.sh | sh | |
| # Pull chroma/ from the live Docker image so the pipeline runs incrementally | |
| - name: Extract ChromaDB from current Heroku image | |
| env: | |
| HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }} | |
| run: | | |
| heroku container:login | |
| docker pull registry.heroku.com/physlibsearch/web || echo "No existing image — starting fresh." | |
| CID=$(docker create registry.heroku.com/physlibsearch/web 2>/dev/null) || true | |
| if [ -n "$CID" ]; then | |
| docker cp "$CID:/app/chroma" . 2>/dev/null || echo "No chroma/ in image — starting fresh." | |
| docker rm "$CID" | |
| fi | |
| # Check if PhysLib has changed since the last successful run. | |
| # The last SHA is stored as a Heroku config var to avoid git commits. | |
| - name: Check PhysLib for new commits | |
| id: check | |
| env: | |
| HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }} | |
| run: | | |
| CURRENT_SHA=$(git ls-remote "$PHYSLIB_REPO" HEAD | cut -f1) | |
| LAST_SHA=$(heroku config:get LAST_PHYSLIB_SHA --app physlibsearch 2>/dev/null || echo "") | |
| echo "current_sha=$CURRENT_SHA" >> "$GITHUB_OUTPUT" | |
| if [ "$CURRENT_SHA" = "$LAST_SHA" ]; then | |
| echo "has_changes=false" >> "$GITHUB_OUTPUT" | |
| echo "PhysLib unchanged at $CURRENT_SHA — nothing to do." | |
| else | |
| echo "has_changes=true" >> "$GITHUB_OUTPUT" | |
| echo "PhysLib changed: $LAST_SHA -> $CURRENT_SHA" | |
| fi | |
| - name: Set up Python | |
| if: steps.check.outputs.has_changes == 'true' | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.12' | |
| cache: pip | |
| - name: Install Python dependencies | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: pip install -r requirements.txt | |
| # PhysLib must be cloned before cache steps so hashFiles() can read lean-toolchain | |
| - name: Clone PhysLib | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: git clone --depth 1 "$PHYSLIB_REPO" physlib | |
| - name: Cache elan toolchains | |
| if: steps.check.outputs.has_changes == 'true' | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.elan | |
| key: elan-${{ hashFiles('physlib/lean-toolchain') }} | |
| - name: Cache PhysLib lake build | |
| if: steps.check.outputs.has_changes == 'true' | |
| uses: actions/cache@v4 | |
| with: | |
| path: physlib/.lake/build | |
| key: physlib-lake-${{ steps.check.outputs.current_sha }} | |
| restore-keys: physlib-lake- | |
| - name: Install elan | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: | | |
| if ! command -v elan &>/dev/null; then | |
| curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | |
| | sh -s -- -y --no-modify-path | |
| fi | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Build PhysLib | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: cd physlib && lake exe cache get && lake build | |
| timeout-minutes: 90 | |
| # jixia must be cloned before its cache step | |
| - name: Clone jixia | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: git clone --depth 1 "$JIXIA_REPO" jixia | |
| - name: Cache jixia build | |
| if: steps.check.outputs.has_changes == 'true' | |
| uses: actions/cache@v4 | |
| with: | |
| path: jixia/.lake/build | |
| # v2: rebuilt against PhysLib's toolchain (see Build jixia below) | |
| key: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}-${{ hashFiles('jixia/lakefile.lean', 'jixia/lakefile.toml') }} | |
| restore-keys: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}- | |
| - name: Build jixia | |
| if: steps.check.outputs.has_changes == 'true' | |
| # jixia reads PhysLib's compiled .olean files, which are version-locked | |
| # to PhysLib's Lean toolchain. Build jixia with the same toolchain so the | |
| # olean headers are compatible (otherwise: "incompatible header"). | |
| run: | | |
| cp physlib/lean-toolchain jixia/lean-toolchain | |
| cd jixia && lake build | |
| timeout-minutes: 30 | |
| - name: Set JIXIA_PATH and LEAN_SYSROOT | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: | | |
| echo "JIXIA_PATH=$(pwd)/jixia/.lake/build/bin/jixia" >> "$GITHUB_ENV" | |
| TOOLCHAIN=$(cat physlib/lean-toolchain) | |
| echo "LEAN_SYSROOT=$HOME/.elan/toolchains/$TOOLCHAIN" >> "$GITHUB_ENV" | |
| # Incremental pipeline — each step skips already-processed items | |
| - name: Create/update schema | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: python3 -m database schema | |
| - name: Load jixia data into PostgreSQL | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: python3 -m database jixia ./physlib "$MODULE_NAMES" | |
| - name: Informalize new declarations | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: python3 -m database informal --batch-size 50 | |
| - name: Embed new declarations into ChromaDB | |
| if: steps.check.outputs.has_changes == 'true' | |
| run: python3 -m database vector-db --batch-size 8 | |
| # Rebuild the Docker image with the updated chroma/ and deploy | |
| - name: Build and release Docker image | |
| if: steps.check.outputs.has_changes == 'true' | |
| env: | |
| HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }} | |
| run: | | |
| heroku container:push web --app physlibsearch | |
| heroku container:release web --app physlibsearch | |
| heroku config:set LAST_PHYSLIB_SHA=${{ steps.check.outputs.current_sha }} --app physlibsearch |