Move Python package to the top level

.dockerignore

@@ -1,7 +1,7 @@
 **/.krun*
 **/.kprove*
 **/.kimp
+**/*venv
 **/dist
 **/.mypy_cache
 **/.pytest_cache
-**/.venv*

.github/workflows/test-pr.yml

@@ -10,9 +10,6 @@ jobs:
     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
@@ -43,7 +40,7 @@ jobs:
         with:
           container-name: ${CONTAINER}
       - name: 'Build and run integration tests'
-        run: docker exec -u user ${CONTAINER} make -C kimp cov-integration
+        run: docker exec -u user ${CONTAINER} make cov-integration
       - name: 'Tear down Docker container'
         if: always()
         run: |

.gitignore

@@ -1,9 +1,6 @@
-.build
-module-imports-graph.svg
-.krun*
-kimp/.kprove*
+/dist/
+__pycache__/
+.coverage
+
+*venv/
 .kimp
-*~
-docker/.image
-dist
-*venv

Makefile

@@ -1,10 +1,28 @@
-K_VERSION   ?= $(shell cat deps/k_release)
-KOMPILE     ?= $(shell which kompile)
+POETRY     := poetry
+POETRY_RUN := $(POETRY) run
 
-default: help
 
-help:
-	@echo "Please read the Makefile."
+default: check test-unit
+
+all: check cov
+
+.PHONY: clean
+clean:
+	rm -rf dist .coverage cov-* .mypy_cache .pytest_cache
+	find -type d -name __pycache__ -prune -exec rm -rf {} \;
+
+.PHONY: build
+build:
+	$(POETRY) build
+
+.PHONY: poetry-install
+poetry-install:
+	$(POETRY) install
+
+
+# Docker
+
+K_VERSION ?= $(shell cat deps/k_release)
 
 .PHONY: docker
 docker: TAG=runtimeverificationinc/imp-semantics:$(K_VERSION)
@@ -14,10 +32,10 @@ docker: package/Dockerfile
 		--file $< \
 		--tag $(TAG)
 
-build: build-kimp
 
-build-kimp: have-k
-	$(MAKE) -C kimp kdist
+# Kompilation
+
+KOMPILE ?= $(shell which kompile)
 
 .PHONY: have-k
 have-k: FOUND_VERSION=$(shell $(KOMPILE) --version | sed -n -e 's/^K version: *v\?\(.*\)$$/\1/p')
@@ -28,3 +46,85 @@ have-k:
 		(echo "Unable to determine K compiler ($(KOMPILE)) version."; exit 1)
 	@[ "$(K_VERSION)" = "$(FOUND_VERSION)" ] || \
 		echo "Unexpected kompile version $(FOUND_VERSION) (expected $(K_VERSION)). Trying anyway..."
+
+kdist: kdist-build
+
+KDIST_ARGS :=
+
+kdist-build: poetry-install have-k
+	$(POETRY_RUN) kdist --verbose build -j2 $(KDIST_ARGS)
+
+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
+
+format: autoflake isort black
+check: check-flake8 check-mypy check-autoflake check-isort check-black
+
+check-flake8: poetry-install
+	$(POETRY_RUN) flake8 src
+
+check-mypy: poetry-install
+	$(POETRY_RUN) mypy src
+
+autoflake: poetry-install
+	$(POETRY_RUN) autoflake --quiet --in-place src
+
+check-autoflake: poetry-install
+	$(POETRY_RUN) autoflake --quiet --check src
+
+isort: poetry-install
+	$(POETRY_RUN) isort src
+
+check-isort: poetry-install
+	$(POETRY_RUN) isort --check src
+
+black: poetry-install
+	$(POETRY_RUN) black src
+
+check-black: poetry-install
+	$(POETRY_RUN) black --check src
+
+
+# Optional tools
+
+SRC_FILES := $(shell find src -type f -name '*.py')
+
+pyupgrade: poetry-install
+	$(POETRY_RUN) pyupgrade --py310-plus $(SRC_FILES)

README.md

@@ -6,7 +6,7 @@ This project showcases the modern methodology of defining language semantics in
 
 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.
+* The `kimp` command-line tool and Python package, that acts as a frontend to the K definitions.
 
 
 ## Trying it out in `docker` (EASY)
@@ -16,76 +16,87 @@ The project defines a Docker image that allows both using `kimp` as-is and hacki
 First off, clone the project and step into its directory:
 
 ```
-git clone https://github.com/runtimeverification/imp-semantics
-cd imp-semantics
+$ git clone https://github.com/runtimeverification/imp-semantics
+$ cd imp-semantics
 ```
 
 Then, build the image:
 
 ```
-make docker TAG=imp-semantics:latest
+$ make docker TAG=imp-semantics:latest
 ```
 
 Run the following command to start a container with an interactive shell:
 
 ```
-docker run --rm -it imp-semantics:latest /bin/bash
+$ docker run --rm -it imp-semantics:latest /bin/bash
 ```
 
 The `examples` folder, as well as a test script `smoke-tests.sh` is already copied into the workspace.
 You can run the tests with:
 
 ```
-./smoke-test.sh
+$ ./smoke-test.sh
 ```
 
 To work with files from the host, run the countainer with a volume mounted.
 For example, the following command starts the container and mounts the current working directory under `~/workspace`, ensuring you can work on the examples and have them transparently available in the container.
 
 ```
-docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) imp-semantics:latest /bin/bash
+$ docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) imp-semantics:latest /bin/bash
 ```
 
 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)
+## 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` Python CLI and library, we recommend using the `poetry` Python build tool. Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation).
 
+### Standalone 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:
+`kimp` is a Python package that can be installed using `pip`, ideally into a virtual environment:
 
 ```
-make build
+$ python -m venv venv
+$ source venv/bin/activate
+(venv) $ pip install .
 ```
 
+After installing the package, the K definitions defined by `kimp` have to be kompiled..
+To kompile the K definitions for both the LLVM (for concrete execution) and Haskell (for symbolic execution) backend, execute:
 
-### Installing
+```
+(venv) $ kdist --verbose build -j2 'imp-semantics.*'
+```
 
-After building the project, you can access the `kimp` CLI via `poetry`:
+After installing the project, you can access the `kimp` CLI:
 
 ```
-poetry run kimp --help
+(venv) $ kimp --help
 ```
 
-use `poetry shell` to avoid prefixing every command with `poetry run`.
 
-Alternatively, you can install `kimp` with `pip` into a virtual environment:
+### For Developers
 
-```
-python -m venv venv
-source venv/bin/activate
-pip install kimp
-```
+Install `poetry` following the instruction [here](https://python-poetry.org/docs/#installation).
+Run `poetry install` to transparently install the package into a virtual environment managed by `poetry`.
+
+Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
+
+* `make`: Check code style and run unit tests (also runs `poetry install`)
+* `make kdist`: Kompile K definitions
+* `make check`: Check code style
+* `make test-unit`: Run unit tests
+* `make format`: Format code
+
+Command `make kdist` needs to be repeated each time the `.k` files under `kimp/src/kimp/kdist/imp-semantics` change,
 
-Within that virtual environment, you can use `kimp` directly.
+Use `poetry run kimp` to execute the `kimp` CLI.
+To avoid prefixing every command with `poetry run`, activate the virtual environment with `poetry shell`.
 
 
 ## Usage
@@ -97,19 +108,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.
-The `Makefile` defines a `build` target that will executed the `kompile` commands for this.
-
-```
-make build
-```
-
-If the `*.k` files in `kimp/src/kimp/kdist/imp-semantics` change, this step needs to be repeated.
-
-
-### Concrete execution
+### Concrete Execution
 
 The K Framework generates an LLVM interpreter from the language semantics. Let is see what it does on a simple example program:
 
@@ -133,7 +132,7 @@ this program adds up the natural numbers up to 10 and should give the following
 ```
 
 
-### Symbolic execution
+### 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: