Add test workflow (#30)

Related: #1

* Add smoke tests
* Add test workflow

.github/actions/with-docker/Dockerfile

@@ -0,0 +1,20 @@
+ARG K_VERSION
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
+
+RUN    apt-get update        \
+    && apt-get upgrade --yes \
+    && apt-get install --yes \
+           curl              \
+    && apt-get clean
+
+ARG USER=user
+ARG GROUP=$USER
+ARG USER_ID=1000
+ARG GROUP_ID=$USER_ID
+
+RUN groupadd -g $GROUP_ID $GROUP && useradd -m -u $USER_ID -s /bin/sh -g $GROUP $USER
+
+USER $USER:$GROUP
+
+ENV PATH=/home/$USER/.local/bin:$PATH
+RUN curl -sSL https://install.python-poetry.org | python3 -

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

@@ -0,0 +1,46 @@
+name: 'With Docker'
+description: 'Start a Docker container with the K development environment set up'
+inputs:
+  container-name:
+    description: 'Docker container name to use'
+    required: true
+    type: string
+runs:
+  using: 'composite'
+  steps:
+  - name: 'Set up Docker'
+    shell: bash {0}
+    run: |
+      set -euxo pipefail
+
+      CONTAINER_NAME=${{ inputs.container-name }}
+      TAG=runtimeverificationinc/${CONTAINER_NAME}
+      DOCKERFILE=${{ github.action_path }}/Dockerfile
+      K_VERSION=$(cat deps/k_release)
+
+      docker build .                       \
+        --file ${DOCKERFILE}               \
+        --build-arg K_VERSION=${K_VERSION} \
+        --tag ${TAG}
+
+  - name: 'Run Docker container'
+    shell: bash {0}
+    run: |
+      set -euxo pipefail
+
+      CONTAINER_NAME=${{ inputs.container-name }}
+      TAG=runtimeverificationinc/${CONTAINER_NAME}
+      WORKDIR=/home/user
+
+      docker run                 \
+        --name ${CONTAINER_NAME} \
+        --rm                     \
+        --interactive            \
+        --tty                    \
+        --detach                 \
+        --user root              \
+        --workdir ${WORKDIR}     \
+        ${TAG}
+
+      docker cp . ${CONTAINER_NAME}:${WORKDIR}
+      docker exec ${CONTAINER_NAME} chown -R user:user ${WORKDIR}

.github/workflows/test-pr.yml

@@ -0,0 +1,65 @@
+name: 'Test PR'
+on:
+  pull_request:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  code-quality-checks:
+    name: 'Code Quality Checks & Unit Tests'
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    defaults:
+      run:
+        working-directory: kimp
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Install Python'
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.10'
+      - name: 'Install Poetry'
+        uses: Gr1N/setup-poetry@v9
+      - name: 'Run code quality checks'
+        run: make check
+      - name: 'Run pyupgrade'
+        run: make pyupgrade
+      - name: 'Run unit tests'
+        run: make cov-unit
+
+  integration-tests:
+    name: 'Integration Tests'
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 5
+    env:
+      CONTAINER: imp-integration-${{ github.sha }}
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: ${CONTAINER}
+      - name: 'Build and run integration tests'
+        run: docker exec -u user ${CONTAINER} make -C kimp cov-integration
+      - name: 'Tear down Docker container'
+        if: always()
+        run: |
+          docker stop --time=0 ${CONTAINER}
+
+  docker-tests:
+    name: 'Docker Tests'
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 5
+    env:
+      TAG: ${{ github.sha }}
+      CONTAINER: imp-docker-${{ github.sha }}
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Build Docker image'
+        run: make docker TAG=${TAG}
+      - name: 'Run smoke tests'
+        run: docker run --rm --name ${CONTAINER} ${TAG} ./smoke-test.sh

Makefile

@@ -7,11 +7,12 @@ help:
 	@echo "Please read the Makefile."
 
 .PHONY: docker
-docker: docker/Dockerfile
-	docker build \
+docker: TAG=runtimeverificationinc/imp-semantics:$(K_VERSION)
+docker: package/Dockerfile
+	docker build . \
 		--build-arg K_VERSION=$(K_VERSION) \
-		-f $< -t runtimeverificationinc/imp-semantics-k:$(K_VERSION) .
-	touch $@
+		--file $< \
+		--tag $(TAG)
 
 build: build-kimp
 
@@ -20,8 +21,6 @@ build-kimp: have-k
 
 .PHONY: have-k
 have-k: FOUND_VERSION=$(shell $(KOMPILE) --version | sed -n -e 's/^K version: *v\?\(.*\)$$/\1/p')
-
-.PHONY: have-k
 have-k:
 	@[ ! -z "$(KOMPILE)" ] || \
 		(echo "K compiler (kompile) not found (use variable KOMPILE to override)."; exit 1)

docker/Dockerfile → package/Dockerfile

@@ -31,11 +31,13 @@ RUN poetry -C /home/k-user/kimp-src build && \
     pip install /home/k-user/kimp-src/dist/*.whl && \
     rm -r /home/k-user/kimp-src && \
     kdist --verbose build -j2
+
 WORKDIR /home/k-user/workspace
+COPY --chown=k-user:k-group examples examples
+COPY --chown=k-user:k-group  ./package/smoke-test.sh .
 
 ENTRYPOINT ["fixuid", "-q"]
 
-
 CMD ["printf", "%s\n",\
      "Welcome to the K Framework!",\
      "",\

package/smoke-test.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+kimp --help
+
+kimp run --verbose --input-file examples/sumto10.imp
+
+kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec
+
+kimp show --verbose IMP-SUM-SPEC sum-spec