Skip to content

Commit 827e46b

Browse files
Add Dockerfile for an image with usable kmir/stable-mir-json installation (#517)
The image contains - `kmir` installed using pip, on the path via `$HOME/.local/bin` - semantics artefacts accessible to `kmir` (within `pip` data directory) - `stable-mir-json` installation in `$HOME/.stable-mir-json`, on the path as a soft-link in `$HOME/.local/bin` The docker image has considerable size (6GB for me) because of the `rustc` installation that `stable-mir-json` refers to. We could consider leaving this part out of the image but there is no easy way to make it much smaller - we have to ship `rustc`. Usage: ``` # in repo root me@mir-semantics$ git submodule update --init me@mir-semantics$ docker buildx build --tag some/tag:$(cat package/version) --file Dockerfile.kmir --build-arg K_VERSION=$(cat deps/k_release) . # takes about 2 minutes and 6GB me@mir-semantics$ docker run --rm -it -v $PWD:/home/kmir/workspace -u $(id -u):$(id -g) some/tag:0.3.108 kmir prove run workspace/kmir/src/tests/integration/data/proving/unchecked-add-spec.k Proving UNCHECKED-ADD-SPEC.unchecked-ADD-spec APRProof: UNCHECKED-ADD-SPEC.unchecked-ADD-spec status: ProofStatus.PASSED admitted: False nodes: 4 pending: 0 failing: 0 vacuous: 0 stuck: 0 terminal: 2 refuted: 0 bounded: 0 execution time: 0s Subproofs: 0 me@mir-semantics$ docker run --rm -it -v $PWD:/home/kmir/workspace -u $(id -u):$(id -g) rv/kmir:0.3.108 stable-mir-json --version rustc 1.85.0-nightly (a2545fd6f 2024-11-28) ``` --------- Co-authored-by: devops <[email protected]>
1 parent aeab055 commit 827e46b

File tree

4 files changed

+68
-3
lines changed

4 files changed

+68
-3
lines changed

Dockerfile.kmir

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
ARG K_VERSION
2+
3+
FROM runtimeverificationinc/kframework-k:ubuntu-jammy-$K_VERSION
4+
5+
ARG K_VERSION
6+
7+
# create non-root user and adjust UID:GID on start-up
8+
# see https://github.com/boxboat/fixuid
9+
RUN addgroup --gid 1000 kmir && \
10+
adduser -uid 1000 --ingroup kmir --home /home/kmir --shell /bin/bash --disabled-password --gecos "" kmir
11+
RUN apt-get install -y curl graphviz python-is-python3 && \
12+
USER=kmir && \
13+
GROUP=kmir && \
14+
curl -SsL https://github.com/boxboat/fixuid/releases/download/v0.6.0/fixuid-0.6.0-linux-amd64.tar.gz | tar -C /usr/local/bin -xzf - && \
15+
chown root:root /usr/local/bin/fixuid && \
16+
chmod 4755 /usr/local/bin/fixuid && \
17+
mkdir -p /etc/fixuid && \
18+
printf "user: $USER\ngroup: $GROUP\n" > /etc/fixuid/config.yml
19+
20+
COPY kmir /kmir
21+
COPY deps/stable-mir-json /deps/stable-mir-json
22+
RUN chown -R kmir:kmir deps/stable-mir-json/
23+
24+
USER kmir:kmir
25+
WORKDIR /home/kmir
26+
ENV K_VERSION=${K_VERSION} \
27+
PATH=/home/kmir/.local/bin:/home/kmir/.cargo/bin:$PATH \
28+
force_color_prompt=yes
29+
30+
# install rustup non-interactively and build
31+
RUN curl https://sh.rustup.rs -sSf | sh -s -- -y --default-toolchain none
32+
33+
# install kmir python parts and K definition/llvm library
34+
RUN cd /kmir && pip install . && kdist build mir-semantics.\*
35+
36+
# build stable-mir-json and install into home
37+
# NB this will modify the default rust toolchain!
38+
# NB assumes submodule has been checked out!
39+
RUN cd /deps/stable-mir-json && \
40+
cargo build && \
41+
cargo build --release && \
42+
cargo run --bin cargo_stable_mir_json -- $PWD && \
43+
ln -s /home/kmir/.stable-mir-json/release.sh /home/kmir/.local/bin/stable-mir-json && \
44+
cargo clean
45+
46+
ENTRYPOINT ["fixuid", "-q"]
47+
48+
CMD printf "%s\n" \
49+
"Welcome to kmir, powered by K framework" \
50+
"" \
51+
"This docker image provides a K-framework installation with the following programs:" \
52+
" * kompile" \
53+
" * krun" \
54+
" * kprove" \
55+
" * kast" \
56+
" * K backend tools (kore-*)" \
57+
" * the pyk library to interact with K programmatically " \
58+
"" \
59+
"as well as a pre-installed kmir tool and stable-mir-json" \
60+
"" \
61+
"To use this docker image, start a container with an interactive shell and" \
62+
"a working directory with your working directory mounted into it, like so:" \
63+
"" \
64+
'user@host$ docker run --rm -it -v "$PWD":/home/kmir/workspace -u $(id -u):$(id -g) <docker-image> /bin/bash' \
65+
""

kmir/pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmir"
7-
version = "0.3.109"
7+
version = "0.3.110"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.109'
3+
VERSION: Final = '0.3.110'

package/version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.3.109
1+
0.3.110

0 commit comments

Comments
 (0)