diff --git a/.github/workflows/cluster-scale-multi-width-ns.yml b/.github/workflows/cluster-scale-multi-width-ns.yml new file mode 100644 index 0000000000..4bcb7f04d2 --- /dev/null +++ b/.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 diff --git a/Blase/README.md b/Blase/README.md index e59bba5994..6b5ec3fe49 100644 --- a/Blase/README.md +++ b/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.