From 3fce5d8b3ef77fdea8d1bd4526ca2dc2f56b26b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 15 Nov 2024 10:00:40 +0000 Subject: [PATCH] Move Python package to the top level, update `README.md` --- kimp/.cruft.json => .cruft.json | 0 .dockerignore | 2 +- kimp/.flake8 => .flake8 | 0 .github/workflows/test-pr.yml | 5 +- .gitignore | 13 +- Makefile | 116 ++++++++++++++++-- README.md | 75 ++++++----- kimp/.gitignore | 3 - kimp/Makefile | 103 ---------------- kimp/README.md | 23 ---- package/Dockerfile | 4 +- kimp/poetry.lock => poetry.lock | 0 kimp/pyproject.toml => pyproject.toml | 0 {kimp/src => src}/kimp/__init__.py | 0 {kimp/src => src}/kimp/__main__.py | 0 {kimp/src => src}/kimp/kdist/__init__.py | 0 .../kimp/kdist/imp-semantics/calls.k | 0 .../kimp/kdist/imp-semantics/expressions.k | 0 .../kdist/imp-semantics/imp-verification.k | 0 .../kimp/kdist/imp-semantics/statements.k | 0 .../kimp/kdist/imp-semantics/variables.k | 0 {kimp/src => src}/kimp/kdist/plugin.py | 0 {kimp/src => src}/kimp/kimp.py | 0 {kimp/src => src}/kimp/py.typed | 0 {kimp/src => src}/tests/__init__.py | 0 .../src => src}/tests/integration/__init__.py | 0 .../tests/integration/test_integration.py | 0 {kimp/src => src}/tests/unit/__init__.py | 0 {kimp/src => src}/tests/unit/test_unit.py | 0 29 files changed, 154 insertions(+), 190 deletions(-) rename kimp/.cruft.json => .cruft.json (100%) rename kimp/.flake8 => .flake8 (100%) delete mode 100644 kimp/.gitignore delete mode 100644 kimp/Makefile delete mode 100644 kimp/README.md rename kimp/poetry.lock => poetry.lock (100%) rename kimp/pyproject.toml => pyproject.toml (100%) rename {kimp/src => src}/kimp/__init__.py (100%) rename {kimp/src => src}/kimp/__main__.py (100%) rename {kimp/src => src}/kimp/kdist/__init__.py (100%) rename {kimp/src => src}/kimp/kdist/imp-semantics/calls.k (100%) rename {kimp/src => src}/kimp/kdist/imp-semantics/expressions.k (100%) rename {kimp/src => src}/kimp/kdist/imp-semantics/imp-verification.k (100%) rename {kimp/src => src}/kimp/kdist/imp-semantics/statements.k (100%) rename {kimp/src => src}/kimp/kdist/imp-semantics/variables.k (100%) rename {kimp/src => src}/kimp/kdist/plugin.py (100%) rename {kimp/src => src}/kimp/kimp.py (100%) rename {kimp/src => src}/kimp/py.typed (100%) rename {kimp/src => src}/tests/__init__.py (100%) rename {kimp/src => src}/tests/integration/__init__.py (100%) rename {kimp/src => src}/tests/integration/test_integration.py (100%) rename {kimp/src => src}/tests/unit/__init__.py (100%) rename {kimp/src => src}/tests/unit/test_unit.py (100%) diff --git a/kimp/.cruft.json b/.cruft.json similarity index 100% rename from kimp/.cruft.json rename to .cruft.json diff --git a/.dockerignore b/.dockerignore index 3982d5c..17b44ae 100644 --- a/.dockerignore +++ b/.dockerignore @@ -1,7 +1,7 @@ **/.krun* **/.kprove* **/.kimp +**/*venv **/dist **/.mypy_cache **/.pytest_cache -**/.venv* diff --git a/kimp/.flake8 b/.flake8 similarity index 100% rename from kimp/.flake8 rename to .flake8 diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 4c8b620..7c55e52 100644 --- a/.github/workflows/test-pr.yml +++ b/.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} maktegration - name: 'Tear down Docker container' if: always() run: | diff --git a/.gitignore b/.gitignore index 2aaf52c..177bfbb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,9 +1,6 @@ -.build -module-imports-graph.svg -.krun* -kimp/.kprove* +/dist/ +__pycache__/ +.coverage + +*venv/ .kimp -*~ -docker/.image -dist -*venv diff --git a/Makefile b/Makefile index 51fd603..ef0dc36 100644 --- a/Makefile +++ b/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) diff --git a/README.md b/README.md index 9a762b9..65a21ed 100644 --- a/README.md +++ b/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: diff --git a/kimp/.gitignore b/kimp/.gitignore deleted file mode 100644 index 98fe5a7..0000000 --- a/kimp/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/dist/ -__pycache__/ -.coverage diff --git a/kimp/Makefile b/kimp/Makefile deleted file mode 100644 index 90b7b9d..0000000 --- a/kimp/Makefile +++ /dev/null @@ -1,103 +0,0 @@ -POETRY := poetry -POETRY_RUN := $(POETRY) run - - -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 - - -# 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 - -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) diff --git a/kimp/README.md b/kimp/README.md deleted file mode 100644 index 1fd23de..0000000 --- a/kimp/README.md +++ /dev/null @@ -1,23 +0,0 @@ -# kimp - - -## Installation - -Prerequsites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`. - -```bash -make build -pip install dist/*.whl -``` - - -## For Developers - -Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets). - -* `make build`: Build wheel -* `make check`: Check code style -* `make format`: Format code -* `make test-unit`: Run unit tests - -For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter. diff --git a/package/Dockerfile b/package/Dockerfile index aa576b1..f47ba0a 100644 --- a/package/Dockerfile +++ b/package/Dockerfile @@ -25,8 +25,8 @@ ENV K_VERSION=${K_VERSION} \ # 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 +# install kimp +COPY --chown=k-user:k-group . /home/k-user/kimp-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 && \ diff --git a/kimp/poetry.lock b/poetry.lock similarity index 100% rename from kimp/poetry.lock rename to poetry.lock diff --git a/kimp/pyproject.toml b/pyproject.toml similarity index 100% rename from kimp/pyproject.toml rename to pyproject.toml diff --git a/kimp/src/kimp/__init__.py b/src/kimp/__init__.py similarity index 100% rename from kimp/src/kimp/__init__.py rename to src/kimp/__init__.py diff --git a/kimp/src/kimp/__main__.py b/src/kimp/__main__.py similarity index 100% rename from kimp/src/kimp/__main__.py rename to src/kimp/__main__.py diff --git a/kimp/src/kimp/kdist/__init__.py b/src/kimp/kdist/__init__.py similarity index 100% rename from kimp/src/kimp/kdist/__init__.py rename to src/kimp/kdist/__init__.py diff --git a/kimp/src/kimp/kdist/imp-semantics/calls.k b/src/kimp/kdist/imp-semantics/calls.k similarity index 100% rename from kimp/src/kimp/kdist/imp-semantics/calls.k rename to src/kimp/kdist/imp-semantics/calls.k diff --git a/kimp/src/kimp/kdist/imp-semantics/expressions.k b/src/kimp/kdist/imp-semantics/expressions.k similarity index 100% rename from kimp/src/kimp/kdist/imp-semantics/expressions.k rename to src/kimp/kdist/imp-semantics/expressions.k diff --git a/kimp/src/kimp/kdist/imp-semantics/imp-verification.k b/src/kimp/kdist/imp-semantics/imp-verification.k similarity index 100% rename from kimp/src/kimp/kdist/imp-semantics/imp-verification.k rename to src/kimp/kdist/imp-semantics/imp-verification.k diff --git a/kimp/src/kimp/kdist/imp-semantics/statements.k b/src/kimp/kdist/imp-semantics/statements.k similarity index 100% rename from kimp/src/kimp/kdist/imp-semantics/statements.k rename to src/kimp/kdist/imp-semantics/statements.k diff --git a/kimp/src/kimp/kdist/imp-semantics/variables.k b/src/kimp/kdist/imp-semantics/variables.k similarity index 100% rename from kimp/src/kimp/kdist/imp-semantics/variables.k rename to src/kimp/kdist/imp-semantics/variables.k diff --git a/kimp/src/kimp/kdist/plugin.py b/src/kimp/kdist/plugin.py similarity index 100% rename from kimp/src/kimp/kdist/plugin.py rename to src/kimp/kdist/plugin.py diff --git a/kimp/src/kimp/kimp.py b/src/kimp/kimp.py similarity index 100% rename from kimp/src/kimp/kimp.py rename to src/kimp/kimp.py diff --git a/kimp/src/kimp/py.typed b/src/kimp/py.typed similarity index 100% rename from kimp/src/kimp/py.typed rename to src/kimp/py.typed diff --git a/kimp/src/tests/__init__.py b/src/tests/__init__.py similarity index 100% rename from kimp/src/tests/__init__.py rename to src/tests/__init__.py diff --git a/kimp/src/tests/integration/__init__.py b/src/tests/integration/__init__.py similarity index 100% rename from kimp/src/tests/integration/__init__.py rename to src/tests/integration/__init__.py diff --git a/kimp/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py similarity index 100% rename from kimp/src/tests/integration/test_integration.py rename to src/tests/integration/test_integration.py diff --git a/kimp/src/tests/unit/__init__.py b/src/tests/unit/__init__.py similarity index 100% rename from kimp/src/tests/unit/__init__.py rename to src/tests/unit/__init__.py diff --git a/kimp/src/tests/unit/test_unit.py b/src/tests/unit/test_unit.py similarity index 100% rename from kimp/src/tests/unit/test_unit.py rename to src/tests/unit/test_unit.py