Tweak README, avoid kompilation output in docker image (#25)

Makefile

@@ -7,10 +7,8 @@ default: help
 help:
 	@echo "Please read the Makefile."
 
-.phony: docker
-docker: docker/.image
-
-docker/.image: docker/Dockerfile.k+pyk
+.PHONY: docker
+docker: docker/Dockerfile.k+pyk
 	docker build \
 		--build-arg K_VERSION=$(K_VERSION) \
 		--build-arg PYK_VERSION=$(PYK_VERSION) \
@@ -32,7 +30,7 @@ build-kimp: have-k
 .build/%-kompiled-haskell: kimp/k-src/%.k $(K_SOURCES)
 	$(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend haskell
 
-.phony: have-k
+.PHONY: have-k
 have-k: FOUND_VERSION = $(shell $(KOMPILE) --version \
 				  | sed -n -e 's/^K version: *v\?\([0-9.]*\)$$/\1/p')
 have-k:

README.md

@@ -17,6 +17,7 @@ First off, clone the project and step into its directory:
 ```
 git clone https://github.com/runtimeverification/imp-semantics
 cd imp-semantics
+git checkout bob2024
 ```
 
 Use the following to start a container with an interactive shell:
@@ -82,6 +83,16 @@ 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/k-src` change, this step needs to be repeated.
+
 ### Concrete execution
 
 The K Framework generates an LLVM interpreter from the language semantics. Let is see what it does on a simple example program:

docker/Dockerfile.k+pyk

@@ -33,14 +33,16 @@ RUN pip install poetry && \
 
 # 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 build && make -C /home/k-user/kimp-src install
-ENV KIMP_LLVM_DIR=/home/k-user/kimp-src/kdist/v${K_VERSION}/llvm       \
-    KIMP_HASKELL_DIR=/home/k-user/kimp-src/kdist/v${K_VERSION}/haskell \
-    KIMP_K_SRC=/home/k-user/kimp-src/k-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
 WORKDIR /home/k-user/workspace
+
 ENTRYPOINT ["fixuid", "-q"]
 
+
 CMD printf "%s\n" \
     "Welcome to the K framework" \
     "" \

kimp/Makefile

@@ -13,7 +13,7 @@ build: kbuild-imp
 
 .PHONY: poetry-install
 poetry-install:
-	$(POETRY) install
+	$(POETRY) install --without dev
 
 .PHONY: kbuild-imp
 kbuild-imp: poetry-install