feat: Blase NS multi-machine batch

.github/workflows/cluster-scale-multi-width-ns.yml

@@ -0,0 +1,232 @@
+# This can be improved by building a docker image of the deps:
+# https://github.com/opencompl/lean-mlir/blob/0048c677755a4544b8e35904549f20d8b48939de/.github/workflows/docker.yml
+# and then running once with that image.
+name: YYY Cluster-Scale Multi-Width (NS)  YYY
+
+
+on:
+  issue_comment:
+    types: [created]
+
+permissions:
+  contents: write
+  id-token: write
+
+jobs:
+  run-batch:
+    if: github.event.issue.pull_request != null && startsWith(github.event.comment.body, "!blase")
+
+    name: Batch Run
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
+      - nscloud-cache-tag-my-custom-cache
+      - nscloud-cache-size-100gb
+      - nscloud-git-mirror-5gb
+      - nscloud-container-image-cache
+      - nscloud-runner-tool-cache-20gb
+
+    strategy:
+      matrix:
+        ibatch: [0, 1, 2]
+        nbatch: [3]
+
+    steps:
+      - name: Setup Ephemeral NS Cluster
+        uses: namespacelabs/nscloud-setup@v0
+
+      # https://namespace.so/docs/reference/github-actions/nscloud-checkout-action
+      - name: Checkout Evaluation Repisitory via NS
+        uses: namespacelabs/nscloud-checkout-action@v7
+        with:
+          repository: "opencompl/evaluation-multi-width-bv"
+          ref: "master"
+          token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
+
+      - name: Setup Ubuntu Dependencies
+        run: |
+          echo "set man-db/auto-update false" | sudo debconf-communicate && sudo dpkg-reconfigure man-db
+          sudo apt-get update
+          sudo apt-get install -y build-essential curl git python3 python3-pip unzip git gettext 
+
+      - name: Setup UV
+        run: |
+          # Install uv (assuming it's Python-based, via pip)
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+
+          # Make uv available in all shells
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+
+      - name: Cache `.elan` folders
+        id: cache-lean
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.elan
+          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+
+      - name: Setup Elan
+        run: |
+          # Install elan (Lean version manager)
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+
+      - name: Make lake available
+        run: |
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache lake.
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: |
+            leanharness/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+
+      - name: Lake Build
+        run: |
+          pushd leanharness; lake build; popd
+
+      - name: Unzip goals
+        run: |
+          unzip -o goals.zip
+
+      - name: Cache Venv
+        id: cache-venv
+        uses: actions/cache@v4
+        with:
+          path: |
+            .venv
+          key: ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+          restore-keys: |
+            ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+
+      - name: Run Minibatch
+        run: |
+          ls
+          pwd
+          set -o pipefail
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+          cp config.full.yaml config.yaml
+          uv tool run snakemake run_minibatch --cores all --config nbatch=${{matrix.nbatch}} ibatch=${{matrix.ibatch}}
+
+      - name: Upload Data As Artifact
+        uses: namespace-actions/upload-artifact@v1
+        with:
+          name: ${{ github.run_id }}-ibatch-${{matrix.ibatch}}
+          retention-days: 1
+          path: |
+            autogenerated/*.jsonl
+          compression-level: 9
+
+
+
+  generate-plots:
+    needs: run-batch
+    name: Generate Reports
+    runs-on:
+      - nscloud-ubuntu-24.04-amd64-16x32-with-cache
+      - nscloud-cache-tag-my-custom-cache
+      - nscloud-cache-size-100gb
+      - nscloud-git-mirror-5gb
+      - nscloud-container-image-cache
+      - nscloud-runner-tool-cache-20gb
+    strategy:
+      matrix:
+        nbatch: [3]
+
+    steps:
+      - name: Setup Ephemeral NS Cluster
+        uses: namespacelabs/nscloud-setup@v0
+
+      - name: Checkout Evaluation Repisitory via NS
+        uses: namespacelabs/nscloud-checkout-action@v7
+        with:
+          repository: "opencompl/evaluation-multi-width-bv"
+          ref: "master"
+          token: ${{ secrets.NSCLOUD_GITHUB_TOKEN }}
+
+      - name: Download Data From Artifact
+        uses: namespace-actions/download-artifact@v1
+        with:
+          path: autogenerated/
+          pattern: ${{ github.run_id }}-ibatch-*
+          merge-multiple: true
+
+      - name: Setup Ubuntu Dependencies
+        run: |
+          echo "set man-db/auto-update false" | sudo debconf-communicate && sudo dpkg-reconfigure man-db
+          sudo apt-get update
+          sudo apt-get install -y build-essential curl git python3 python3-pip unzip git gettext 
+
+      - name: Setup UV
+        run: |
+          # Install uv (assuming it's Python-based, via pip)
+          curl -LsSf https://astral.sh/uv/install.sh | sh
+
+          # Make uv available in all shells
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+
+      - name: Cache `.elan` folders
+        id: cache-lean
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.elan
+          key: ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-elan-${{ hashFiles('leanharness/lean-toolchain') }}
+
+      - name: Setup Elan
+        run: |
+          # Install elan (Lean version manager)
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+
+      - name: Cache lake.
+        id: cache-lake
+        uses: actions/cache@v4
+        with:
+          path: |
+            leanharness/.lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-${{ hashFiles('leanharness/lake-manifest.json') }}
+
+      - name: Make lake available
+        run: |
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Lake Build
+        run: |
+          pushd leanharness; lake build; popd
+
+
+      - name: Unzip goals
+        run: |
+          unzip -o goals.zip
+
+      - name: Cache Venv
+        id: cache-venv
+        uses: actions/cache@v4
+        with:
+          path: |
+            .venv
+          key: ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+          restore-keys: |
+            ${{ runner.os }}-venv-${{ hashFiles('uv.lock', 'pyproject.toml') }}
+
+
+      - name: Run Plotting Script
+        run: |
+          find autogenerated/ 
+
+          cp config.full.yaml config.yaml
+          sed -i 's@upload: False@upload: True@g' config.yaml
+          # only allow rules to collate 'jsonl' and to plot.
+          uv tool run snakemake all --cores all \
+            --config nbatch=${{matrix.nbatch}} \
+            --allowed-rules plot epoch_jsonl --cores all

Blase/README.md

@@ -16,6 +16,8 @@ For stable releases, please change the `rev` to the desired version tag.
 
 #### Algorithms Improvements TODO
 
+- [ ] Write a tactic that takes a goal state with BVs and generalizes them to an arbitrary width. 
+      Call this `bv_abstract`.
 - [ ] Add evaluation from Sam Coward.
 - [ ] Add evaluation from Lean's bitvector suite.
 - [ ] Add right shift and division support by eliminating into left-shift and multiplication.