Migrate to kdist (#29)

Replace the `kbuild`-based build logic by a `kdist` plugin.

.dockerignore

@@ -2,7 +2,6 @@
 **/.kprove*
 **/.kimp
 **/dist
-**/kdist
 **/.mypy_cache
 **/.pytest_cache
-**/.venv*
+**/.venv*

.gitignore

@@ -1,11 +1,9 @@
 .build
 module-imports-graph.svg
-tests/specs/verification-kompiled/*
 .krun*
 kimp/.kprove*
 .kimp
 *~
 docker/.image
 dist
-kdist
-*venv
+*venv

Makefile

@@ -13,24 +13,15 @@ docker: docker/Dockerfile
 		-f $< -t runtimeverificationinc/imp-semantics-k:$(K_VERSION) .
 	touch $@
 
-K_SOURCES = $(wildcard kimp/k-src/*.k)
-TARGETS   = $(patsubst %.k,.build/%-kompiled,$(notdir $(K_SOURCES)))
+build: build-kimp
 
-build: build-llvm build-haskell build-kimp
-
-build-llvm: have-k $(TARGETS:=-llvm)
-build-haskell: have-k $(TARGETS:=-haskell)
 build-kimp: have-k
-	$(MAKE) -C kimp build
+	$(MAKE) -C kimp kdist
 
-.build/%-kompiled-llvm: kimp/k-src/%.k $(K_SOURCES)
-	$(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend llvm
-.build/%-kompiled-haskell: kimp/k-src/%.k $(K_SOURCES)
-	$(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend haskell
+.PHONY: have-k
+have-k: FOUND_VERSION=$(shell $(KOMPILE) --version | sed -n -e 's/^K version: *v\?\(.*\)$$/\1/p')
 
 .PHONY: have-k
-have-k: FOUND_VERSION = $(shell $(KOMPILE) --version \
-				  | sed -n -e 's/^K version: *v\?\([0-9.]*\)$$/\1/p')
 have-k:
 	@[ ! -z "$(KOMPILE)" ] || \
 		(echo "K compiler (kompile) not found (use variable KOMPILE to override)."; exit 1)

README.md

@@ -8,9 +8,10 @@ KIMP consists of two major components:
 * The K definition of IMP;
 * The `kimp` command-line tool and Python package, that acts as a frontend to the K definition.
 
+
 ## Trying it out in `docker` (EASY)
 
-We have prepared a docker image that allows both using `kimp` as-is and hacking on it.
+We have prepared a Docker image that allows both using `kimp` as-is and hacking on it.
 
 First off, clone the project and step into its directory:
 
@@ -30,29 +31,24 @@ This command will download the docker image and mount the current working direct
 
 If everything is up and running, feel free to jump straight to the **Usage** section below. If you don't want to use `docker`, read the next section to build `kimp` manually.
 
+
 ## Installation instructions (ADVANCED)
 
 ### Prerequisites
 
 Make sure the K Framework is installed and is available on `PATH`. To install K, follow the official [Quick Start](https://github.com/runtimeverification/k#quick-start) instructions.
 
-To build the `kimp` Ptyhon CLI and library, we recommend using the `poetry` Python build tool. Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation).
+To build the `kimp` Python CLI and library, we recommend using the `poetry` Python build tool. Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation).
+
 
 ### Building
 
 To build the whole codebase, inclusing the `kimp` CLI and the K definition with both backends, LLVM (for concrete execution) and Haskell (for symbolic execution), execute:
+
 ```
 make build
 ```
 
-The `kimp` executable is a relatively thin wrapper for a number of generic K tools. These tools need access to the output of the K compiler that were produced at the previous step. The most robust way to point `kimp` to the K compiler output is by setting the following three environment variables:
-
-```
-export K_VERSION=$(cat deps/k_release)
-export KIMP_LLVM_DIR=$(realpath ./kimp/kdist/v${K_VERSION}/llvm)
-export KIMP_HASKELL_DIR=$(realpath ./kimp/kdist/v${K_VERSION}/haskell)
-export KIMP_K_SRC=$(realpath ./kimp/k-src)
-```
 
 ### Installing
 
@@ -69,7 +65,7 @@ Alternatively, you can install `kimp` with `pip` into a virtual environment:
 ```
 python -m venv venv
 source venv/bin/activate
-make -C kimp install # this calls pip for you
+pip install kimp
 ```
 
 Within that virtual environment, you can use `kimp` directly.
@@ -83,6 +79,7 @@ Within that virtual environment, you can use `kimp` directly.
 
 Run `kimp --help` to see the available commands and their arguments. Let us now give examples for both concrete executing and proving:
 
+
 ### Preparation
 
 The K files need to be compiled before anything can be executed.
@@ -91,7 +88,9 @@ The `Makefile` defines a `build` target that will executed the `kompile` command
 ```
 make build
 ```
-If the `*.k` files in `kimp/k-src` change, this step needs to be repeated.
+
+If the `*.k` files in `kimp/src/kimp/kdist/imp-semantics` change, this step needs to be repeated.
+
 
 ### Concrete execution
 
@@ -116,6 +115,7 @@ this program adds up the natural numbers up to 10 and should give the following
 </generatedTop>
 ```
 
+
 ### Symbolic execution
 
 The K Framework is equipped with a symbolic execution backend that can be used to prove properties of programs. The properties to prove are formulated as K claims, and are essentially statements that one state always rewrites to another state if certain conditions hold. An example K claim that formulates an inductive invariant about the summation program we've executed before can be found in `examples/specs/imp-sum-spec.k`. Let us ask the prover to check this claim:
@@ -127,16 +127,11 @@ kimp prove examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec
 That command would run for some time and output the symbolic execution trace to a file upon completion. We can pretty-print the trace:
 
 ```
-kimp show-kcfg IMP-SUM-SPEC sum-spec
+kimp show IMP-SUM-SPEC sum-spec
 ```
 
 or even explore it interactively in a terminal user interface
 
 ```
-kimp view-kcfg IMP-SUM-SPEC sum-spec
+kimp view IMP-SUM-SPEC sum-spec
 ```
-
-
-
-
-

docker/Dockerfile

@@ -23,15 +23,14 @@ ENV K_VERSION=${K_VERSION} \
     force_color_prompt=yes
 
 # install poetry
-RUN pip install poetry
+RUN curl -sSL https://install.python-poetry.org | python3 -
 
 # install kimp and set env vars for it
 COPY --chown=k-user:k-group ./kimp /home/k-user/kimp-src
-RUN make -C /home/k-user/kimp-src install && \
-    rm -r /home/k-user/kimp-src
-ENV KIMP_LLVM_DIR=/home/k-user/workspace/kimp/kdist/v${K_VERSION}/llvm       \
-    KIMP_HASKELL_DIR=/home/k-user/workspace/kimp/kdist/v${K_VERSION}/haskell \
-    KIMP_K_SRC=/home/k-user/workspace/kimp/k-src
+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
 
 ENTRYPOINT ["fixuid", "-q"]

kimp/Makefile

@@ -1,29 +1,69 @@
 POETRY     := poetry
 POETRY_RUN := $(POETRY) run
 
-default: build
+
+default: check test-unit
+
+all: check cov
 
 .PHONY: clean
 clean:
-	rm -rf dist .mypy_cache .pytest_cache
+	rm -rf dist .coverage cov-* .mypy_cache .pytest_cache
 	find -type d -name __pycache__ -prune -exec rm -rf {} \;
 
 .PHONY: build
-build: kbuild-imp
+build:
+	$(POETRY) build
 
 .PHONY: poetry-install
 poetry-install:
-	$(POETRY) install --without dev
+	$(POETRY) install
 
-.PHONY: kbuild-imp
-kbuild-imp: poetry-install
-	$(POETRY) run kbuild kompile llvm
-	$(POETRY) run kbuild kompile haskell
 
-.PHONY: install
-install: poetry-install
-	$(POETRY) build
-	pip install dist/*.whl
+# Kompilation
+
+kdist: kdist-build
+
+kdist-build: poetry-install
+	$(POETRY_RUN) kdist --verbose build -j2
+
+kdist-clean: poetry-install
+	$(POETRY_RUN) kdist clean
+
+
+# Tests
+
+TEST_ARGS :=
+
+test: test-all
+
+test-all: poetry-install
+	$(POETRY_RUN) pytest src/tests --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+
+test-unit: poetry-install
+	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
+
+test-integration: poetry-install
+	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+
+
+# Coverage
+
+COV_ARGS :=
+
+cov: cov-all
+
+cov-%: TEST_ARGS += --cov=kimp --no-cov-on-fail --cov-branch --cov-report=term
+
+cov-all: TEST_ARGS += --cov-report=html:cov-all-html $(COV_ARGS)
+cov-all: test-all
+
+cov-unit: TEST_ARGS += --cov-report=html:cov-unit-html $(COV_ARGS)
+cov-unit: test-unit
+
+cov-integration: TEST_ARGS += --cov-report=html:cov-integration-html $(COV_ARGS)
+cov-integration: test-integration
+
 
 # Checks and formatting
 

kimp/pyproject.toml

@@ -10,13 +10,16 @@ authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
+[tool.poetry.scripts]
+kimp = "kimp.__main__:main"
+
+[tool.poetry.plugins.kdist]
+imp-semantics = "kimp.kdist.plugin"
+
 [tool.poetry.dependencies]
 python = "^3.10"
 kframework = "v7.1.170"
 
-[tool.poetry.scripts]
-kimp = "kimp.__main__:main"
-
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"
 black = "*"