Publish Docker image + Example CI WF + Upload to dockerhub

.github/workflows/release.yml

@@ -0,0 +1,43 @@
+name: "Release KMIR"
+
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+  release:
+    runs-on: [self-hosted, linux, normal]
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          submodules: recursive
+      - name: 'Setup Docker Buildx'
+        uses: docker/setup-buildx-action@v3.10.0
+
+      - name: 'Login to Docker Hub'
+        uses: docker/login-action@v3.4.0
+        with:
+          username: ${{ vars.DOCKERHUB_USERNAME }}
+          password: ${{ secrets.DOCKERHUB_PASSWORD }}
+
+      - name: Set Image Name
+        id: set-image-name
+        run: |
+          echo "image-name=runtimeverificationinc/kmir" >> $GITHUB_OUTPUT
+          echo "k-version=$(cat deps/k_release)" >> $GITHUB_OUTPUT
+          echo "kmir-version=$(cat package/version)" >> $GITHUB_OUTPUT
+          echo "short-sha=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT
+
+      - name: Build Kmir Container
+        uses: docker/build-push-action@v6
+        with:
+          context: .
+          file: Dockerfile.kmir
+          platforms: linux/amd64
+          push: true
+          build-args: |
+            K_VERSION=${{ steps.set-image-name.outputs.k-version }}
+          tags: ${{ steps.set-image-name.outputs.image-name }}:ubuntu-jammy-${{ steps.set-image-name.outputs.kmir-version }}
+

.github/workflows/test.yml

@@ -123,3 +123,83 @@ jobs:
       - name: 'Tear down Docker'
         if: always()
         run: docker stop --time 0 mir-smir-ci-${GITHUB_SHA}
+
+  test-kmir-image:
+    name: Test Kmir Image
+    needs: [ unit-tests, version-bump ]
+    runs-on: ubuntu-latest
+    env:
+      container_name: "kmir-${{ github.run_id }}"
+    outputs:
+      image-name: ${{ steps.set-image-name.outputs.image-name }}
+      k-version: ${{ steps.set-image-name.outputs.k-version }}
+      kmir-version: ${{ steps.set-image-name.outputs.kmir-version }}
+      short-sha: ${{ steps.set-image-name.outputs.short-sha }}
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Docker Buildx
+        uses: docker/setup-buildx-action@v3.10.0
+
+      - name: Set Image Name Parameters
+        id: set-image-name
+        run: |
+          echo "image-name=ghcr.io/runtimeverification/mir-semantics/kmir" >> $GITHUB_OUTPUT
+          echo "k-version=$(cat deps/k_release)" >> $GITHUB_OUTPUT
+          echo "kmir-version=$(cat package/version)" >> $GITHUB_OUTPUT
+          echo "short-sha=$(git rev-parse --short HEAD)" >> $GITHUB_OUTPUT
+
+      - name: Build Kmir Container
+        uses: docker/build-push-action@v6
+        with:
+          context: .
+          file: Dockerfile.kmir
+          platforms: linux/amd64
+          push: false
+          load: true
+          build-args: |
+            K_VERSION=${{ steps.set-image-name.outputs.k-version }}
+          tags: ${{ steps.set-image-name.outputs.image-name }}:ubuntu-jammy-${{ steps.set-image-name.outputs.kmir-version }}-${{ steps.set-image-name.outputs.short-sha }}
+
+      - name: Container Sanity Check
+        run: |
+          # Create output directories for each test
+          for k_file in kmir/src/tests/integration/data/*/*-spec.k; do
+            proof_dir="$(dirname ${k_file})/proofs"
+            mkdir -p "${proof_dir}"
+            chmod 777 "${proof_dir}"
+          done
+
+          # Start Container
+          docker run --detach --rm -t \
+            --name ${{ env.container_name }} \
+            -v $PWD:/home/kmir/workspace \
+            -w /home/kmir/workspace \
+            ${{ steps.set-image-name.outputs.image-name }}:ubuntu-jammy-${{ steps.set-image-name.outputs.kmir-version }}-${{ steps.set-image-name.outputs.short-sha }} \
+            /bin/bash
+
+          # Run all tests in a single exec command to maintain fixuid context
+          docker exec \
+            -w /home/kmir/workspace \
+            ${{ env.container_name }} \
+            /bin/bash -c '
+              for k_file in kmir/src/tests/integration/data/*/*-spec.k; do
+                echo "Running ${k_file}"
+                proof_dir="$(dirname ${k_file})/proofs"
+                if ! kmir prove run "${k_file}" --proof-dir "${proof_dir}" 2>&1; then
+                  echo "Proof failed for ${k_file}"
+                fi
+              done
+            '
+
+          # Print test results
+          echo "Test results:"
+          find kmir/src/tests/integration/data -name "proofs" -type d -exec echo {} >> GITHUB_STEP_SUMMARY \;
+
+      - name: Tear Down Container
+        if: always()
+        run: docker stop ${{ env.container_name }}
+

Dockerfile.kmir

@@ -6,8 +6,8 @@
 
 # create non-root user and adjust UID:GID on start-up
 # see https://github.com/boxboat/fixuid
-RUN addgroup --gid 1000 kmir && \
-    adduser -uid 1000 --ingroup kmir --home /home/kmir --shell /bin/bash --disabled-password --gecos "" kmir
+RUN addgroup --gid 1111 kmir && \
+    adduser -uid 1111 --ingroup kmir --home /home/kmir --shell /bin/bash --disabled-password --gecos "" kmir
 RUN apt-get install -y curl graphviz python-is-python3 && \
     USER=kmir && \
     GROUP=kmir && \
@@ -23,9 +23,15 @@
 
 USER kmir:kmir
 WORKDIR /home/kmir
+# Set Env variables for Building
 ENV K_VERSION=${K_VERSION} \
     PATH=/home/kmir/.local/bin:/home/kmir/.cargo/bin:$PATH \
     force_color_prompt=yes
+# Set Env Variables every time a new shell is opened (e.g. when using 'docker exec')
+RUN echo "export K_VERSION=${K_VERSION}" >> /home/kmir/.bash_profile && \
+    echo "export PATH=/home/kmir/.local/bin:/home/kmir/.cargo/bin:\$PATH" >> /home/kmir/.bash_profile && \
+    echo "export force_color_prompt=yes" >> /home/kmir/.bash_profile && \
+    echo "source /home/kmir/.bash_profile" >> /home/kmir/.bashrc
 
 # install rustup non-interactively and build
 RUN curl https://sh.rustup.rs -sSf | sh -s -- -y --default-toolchain none
@@ -42,10 +48,10 @@
     cargo run --bin cargo_stable_mir_json -- $PWD && \
     ln -s /home/kmir/.stable-mir-json/release.sh /home/kmir/.local/bin/stable-mir-json && \
     cargo clean
-
+# Fixuid is helpful for 1 time executions of docker containers but is not helpful when relying on `docker exec` 
 ENTRYPOINT ["fixuid", "-q"]
 
 CMD printf "%s\n" \
     "Welcome to kmir, powered by K framework" \
     "" \
     "This docker image provides a K-framework installation with the following programs:" \

flake.nix

@@ -1,5 +1,5 @@
 {
-  description = "mir-semantics - ";
+  description = "kmir - ";
   inputs = {
     k-framework.url = "github:runtimeverification/k/v7.1.229";
     nixpkgs.follows = "k-framework/nixpkgs";
@@ -15,7 +15,7 @@
           poetry2nix =
             inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = prev; };
           in {
-          mir-semantics = poetry2nix.mkPoetryApplication {
+          kmir = poetry2nix.mkPoetryApplication {
             python = prev.python310;
             projectDir = ./kmir;
             overrides = poetry2nix.overrides.withDefaults
@@ -41,8 +41,8 @@
         };
       in {
         packages = rec {
-          inherit (pkgs) mir-semantics;
-          default = mir-semantics;
+          inherit (pkgs) kmir;
+          default = kmir;
         };
       }) // {
         overlay = nixpkgs.lib.composeManyExtensions allOverlays;

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.113"
+version = "0.3.114"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.113'
+VERSION: Final = '0.3.114'

package/version

@@ -1 +1 @@
-0.3.113
+0.3.114