Ci/use z3 image (#86)

* Move to using a standard z3 pre-built image

* Updating Kontrol CI to use prebuild docker image of z3. Updating Published Kontrol iamge to use same version of Z3 Kontrol is built with

* Set Version: 0.1.21

* Set Z3 version in docker tests

* NOT PLURAL!

* Remove extra line

* Resolve unauthroized access

* ARGs

* Adding suggested additional line to file

* Set Version: 0.1.24

* Update k_release

* Set Version: 0.1.25

* Update Dockerfile

* Update Dockerfile

* Set Version: 0.1.26

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

.github/actions/with-docker/action.yml

@@ -53,15 +53,11 @@ runs:
 
       USER=github-user
       GROUP=${USER}
-      Z3_VERSION=4.12.1
+      Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat deps/k_release)
       USER_ID=1000
       GROUP_ID=${USER_ID}
 
-      docker build .                           \
-        --file .github/workflows/Dockerfile.z3 \
-        --tag z3:${Z3_VERSION}                 \
-
       docker build . --file ${DOCKERFILE}        \
         --tag ${TAG_NAME}                        \
         --build-arg USER_ID=${USER_ID}           \

.github/workflows/Dockerfile

@@ -6,7 +6,7 @@ ARG LLVM_VERSION
 FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
 
 ARG Z3_VERSION
-FROM z3:${Z3_VERSION} as Z3
+FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
 
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}

.github/workflows/test-pr.yml

@@ -134,6 +134,13 @@ jobs:
         uses: actions/checkout@v3
         with:
           fetch-depth: 0
+
+      - name: Login to Docker Hub
+        uses: docker/login-action@v3
+        with:
+          username: rvdockerhub
+          password: ${{ secrets.DOCKERHUB_PASSWORD }}
+
       - name: 'Set environment'
         run: |
           echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}" >> ${GITHUB_ENV}
@@ -144,7 +151,8 @@ jobs:
       - name: 'Build Docker image'
         run: |
           K_VERSION=$(cat deps/k_release)
-          docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION}
+          Z3_VERSION=$(cat deps/z3)
+          docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}
       - name: 'Start Docker container'
         run: |
           docker run                          \

Dockerfile

@@ -1,8 +1,15 @@
+ARG Z3_VERSION
+ARG K_VERSION
+FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
+
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
 ARG PYTHON_VERSION=3.10
 
+# Upgrade z3 to match the version Kontrol was built with not minimum version used in K.
+COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+
 RUN    apt-get -y update             \
     && apt-get -y install            \
          autoconf                    \
@@ -37,4 +44,4 @@ USER user
 ENV PATH=/home/user/.local/bin:${PATH}
 RUN    pip install ./kontrol \
     && rm -rf kontrol        \
-    && CXX=clang++-14 kevm-dist --verbose build -j4
+    && CXX=clang++-14 kevm-dist --verbose build -j4

deps/z3

@@ -0,0 +1,2 @@
+4.12.1
+

package/version

@@ -1 +1 @@
-0.1.25
+0.1.26

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.25"
+version = "0.1.26"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.25'
+VERSION: Final = '0.1.26'