Merge branch 'master' into schedule

Pi-Squared-Inc · Apr 11, 2024 · c72a46f · c72a46f
2 parents 7064cce + b758bd2
commit c72a46f
Show file tree

Hide file tree

Showing 23 changed files with 65 additions and 380 deletions.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -9,38 +9,12 @@ concurrency:
 
 jobs:
 
-  version-bump:
-    name: 'Version Bump'
-    runs-on: [self-hosted, linux, flyweight-ephemeral]
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          # fetch-depth 0 means deep clone the repo
-          fetch-depth: 0
-          ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name devops
-          git config user.email [email protected]
-      - name: 'Update version'
-        run: |
-          og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
-          ./package/version.sh bump ${og_version}
-          ./package/version.sh sub
-          new_version=$(cat package/version)
-          sed --in-place "s/^VERSION: Final = '.*'$/VERSION: Final = '${new_version}'/" kevm-pyk/src/kevm_pyk/__init__.py
-          git add --update && git commit --message "Set Version: ${new_version}" || true
-      - name: 'Push updates'
-        run: git push origin HEAD:${GITHUB_HEAD_REF}
-
   kevm-pyk-code-quality-checks:
     name: 'Code Quality Checks'
-    runs-on: [self-hosted, linux, flyweight-ephemeral]
+    runs-on: [self-hosted, linux, flyweight]
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - uses: actions/setup-python@v4
         with:
             python-version: "3.10"
@@ -54,10 +28,10 @@ jobs:
   kevm-pyk-unit-tests:
     needs: kevm-pyk-code-quality-checks
     name: 'Unit Tests'
-    runs-on: [self-hosted, linux, normal-ephemeral]
+    runs-on: [self-hosted, linux, normal]
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: true
           fetch-depth: 0
@@ -73,10 +47,10 @@ jobs:
   kevm-pyk-profile:
     needs: kevm-pyk-code-quality-checks
     name: 'Profiling'
-    runs-on: [self-hosted, linux, normal-ephemeral]
+    runs-on: [self-hosted, linux, normal]
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           fetch-depth: 0
@@ -97,7 +71,7 @@ jobs:
     timeout-minutes: 45
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           fetch-depth: 0
@@ -108,7 +82,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.haskell evm-semantics.kllvm evm-semantics.kllvm-runtime'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.kllvm evm-semantics.kllvm-runtime'
       - name: 'Test integration'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
@@ -119,79 +93,3 @@ jobs:
         if: always()
         run: |
           docker stop --time=0 kevm-ci-concrete-${{ github.sha }}
-
-  test-prove:
-    name: 'Build and Test KEVM proofs'
-    needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, fast]
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - test-suite: 'test-prove-kprove'
-            test-args:
-            timeout: 45
-          - test-suite: 'test-prove-pyk'
-            test-args:
-            timeout: 180
-          - test-suite: 'test-prove-pyk'
-            test-args: '--use-booster'
-            timeout: 150
-    timeout-minutes: ${{ matrix.timeout }}
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
-        with:
-          container-name: kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
-      - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
-      - name: 'Build distribution'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell'
-      - name: 'Prove Haskell'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=4"
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
-
-  nix:
-    name: 'Nix'
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - runner: normal
-          - runner: macos-13
-          - runner: ARM64
-    needs: kevm-pyk-code-quality-checks
-    runs-on: ${{ matrix.runner }}
-    timeout-minutes: 60
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          # Check out pull request HEAD instead of merge commit.
-          ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Install Nix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v25
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.19.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-            substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/cachix-action@v14
-        with:
-          name: k-framework
-          authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
-      - name: 'Build KEVM'
-        run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs
-      - name: 'Test KEVM'
-        run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kevm-test
diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
@@ -44,26 +44,5 @@ jobs:
           BKP_VERSION=$(git -C kevm-pyk/src/kevm_pyk/kproj/plugin rev-parse HEAD)
           echo ${BKP_VERSION} > deps/blockchain-k-plugin_release
           git add deps/blockchain-k-plugin_release && git commit -m "deps/blockchain-k-plugin_release: sync release file version ${BKP_VERSION}" || true
-      - name: 'Install Nix/Cachix'
-        uses: cachix/install-nix-action@v19
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-      - uses: cachix/cachix-action@v12
-        with:
-          name: k-framework
-          authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
-      - name: 'Update nix flake inputs'
-        run: |
-          K_VERSION=$(cat deps/k_release)
-          BKP_VERSION=$(cat deps/blockchain-k-plugin_release)
-          PYK_VERSION=$(cat deps/pyk_release)
-          sed -i 's!    k-framework.url = "github:runtimeverification/k/[v0-9\.]*"!    k-framework.url = "github:runtimeverification/k/v'"${K_VERSION}"'"!' flake.nix
-          sed -i 's!    blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/[0-9a-f]*"!    blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/'"${BKP_VERSION}"'"!' flake.nix
-          sed -i 's!    pyk.url = "github:runtimeverification/pyk/[v0-9\.]*"!    pyk.url = "github:runtimeverification/pyk/'"${PYK_VERSION}"'"!' flake.nix
-          nix run .#update-from-submodules
-          nix flake update
-          git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true
       - name: 'Push updates'
         run: git push
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-6.3.75
+6.3.77
diff --git a/deps/pyk_release b/deps/pyk_release
@@ -1 +1 @@
-v0.1.777
+v0.1.778
diff --git a/flake.lock b/flake.lock