Skip to content

Commit 63ddb5c

Browse files
cgwalterscgwalters
authored
Two devenv patches (#93)
* devenv: Drop goose from tools Goose is not currently needed in the devenv image. Assisted-by: OpenCode (Claude Sonnet 4) Signed-off-by: Colin Walters <walters@verbum.org> * devenv: Add Kani and extract shared installation scripts Add Kani formal verification tool - a bounded model checker for Rust that can verify safety properties and absence of undefined behavior. Kani requires rustup because it bundles a specific nightly toolchain. Also deduplicate the installation logic between c10s and debian Containerfiles by extracting into shared shell scripts: - fetch-tools.sh: Downloads bcvk and scorecard binaries - install-rust.sh: Installs rustup/cargo system-wide to /usr/local - install-kani.sh: Installs kani formal verification tool Key changes: - Add rustup symlink at $CARGO_HOME/bin/rustup (required for rustup's self-update check which looks for itself there) - Add new 'kani' build stage that compiles kani-verifier and runs setup - Set KANI_HOME=/usr/local/kani for system-wide installation - Copy kani bundle (compiler, libraries, CBMC) to final image The kani version is renovate-managed via the kaniversion ARG. Assisted-by: OpenCode (Claude Sonnet 4) Signed-off-by: Colin Walters <walters@verbum.org> --------- Signed-off-by: Colin Walters <walters@verbum.org>
1 parent 1a0c1d7 commit 63ddb5c

6 files changed

Lines changed: 125 additions & 124 deletions

File tree

‎devenv/.dockerignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,6 @@
1212
!build-deps-debian.txt
1313
!build-deps-c10s.txt
1414
!devenv-init.sh
15+
!fetch-tools.sh
16+
!install-rust.sh
17+
!install-kani.sh

‎devenv/Containerfile.c10s‎

Lines changed: 18 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -26,73 +26,24 @@ dnf -y makecache
2626
EORUN
2727

2828
FROM base as tools
29-
# renovate: datasource=github-releases depName=block/goose
30-
ARG gooseversion=v1.11.1
3129
# renovate: datasource=github-releases depName=bootc-dev/bcvk
3230
ARG bcvkversion=v0.9.0
3331
# renovate: datasource=github-releases depName=ossf/scorecard
3432
ARG scorecardversion=v5.1.1
35-
RUN <<EORUN
36-
set -xeuo pipefail
37-
arch=$(arch)
38-
39-
rm -vrf /usr/local/bin/*
40-
41-
# goose is a single static binary
42-
target=goose-${arch}-unknown-linux-gnu.tar.bz2
43-
/bin/time -f '%E %C' curl -fLO https://github.com/block/goose/releases/download/$gooseversion/$target
44-
tar xvjf $target
45-
mv goose /usr/local/bin/goose
46-
47-
## Other tools
48-
49-
# bcvk
50-
if test "${arch}" = x86_64; then
51-
td=$(mktemp -d)
52-
(
53-
cd $td
54-
target=bcvk-${arch}-unknown-linux-gnu
55-
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
56-
tar xvzf $target.tar.gz
57-
mv $target /usr/local/bin/bcvk
58-
)
59-
rm -rf $td
60-
else
61-
echo bcvk unavailable for $arch
62-
fi
63-
64-
# scorecard (OpenSSF security scanner)
65-
td=$(mktemp -d)
66-
(
67-
cd $td
68-
# Map arch to scorecard naming convention
69-
case "${arch}" in
70-
x86_64) scarch=amd64 ;;
71-
aarch64) scarch=arm64 ;;
72-
*) echo "scorecard unavailable for $arch"; exit 0 ;;
73-
esac
74-
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
75-
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
76-
tar xvzf $target
77-
mv scorecard /usr/local/bin/scorecard
78-
)
79-
rm -rf $td
80-
EORUN
33+
COPY fetch-tools.sh /run/src/
34+
RUN bcvkversion=$bcvkversion scorecardversion=$scorecardversion /run/src/fetch-tools.sh
8135

8236
FROM base as rust
83-
RUN <<EORUN
84-
set -xeuo pipefail
85-
# Setup rust; the idea here though is we install system-wide into /usr/local
86-
# as if it was packaged.
87-
export RUSTUP_HOME=/usr/local/rustup
88-
export CARGO_HOME=/usr/local/cargo
89-
# Install Rust system-wide
90-
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
91-
# Move binaries to /usr/local/bin (system-managed, root-owned)
92-
mv /usr/local/cargo/bin/* /usr/local/bin/
93-
# Nothing really left here
94-
rm -vrf /usr/local/cargo/bin
95-
EORUN
37+
COPY install-rust.sh /run/src/
38+
RUN /run/src/install-rust.sh
39+
40+
# Kani formal verification tool - requires rustup for toolchain management
41+
FROM rust as kani
42+
# renovate: datasource=crate depName=kani-verifier
43+
ARG kaniversion=0.67.0
44+
RUN dnf install -y gcc && dnf clean all
45+
COPY install-kani.sh /run/src/
46+
RUN kaniversion=$kaniversion /run/src/install-kani.sh
9647

9748
# This builds the image.
9849
# Build this using `just devenv-build-c10s` from the root of the repository.
@@ -110,10 +61,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
11061

11162
# Copy in the binaries from our tools container image
11263
COPY --from=tools /usr/local/bin/* /usr/local/bin/
113-
COPY --from=rust /usr/local/bin/* /usr/local/bin/
114-
COPY --from=rust /usr/local/rustup /usr/local/rustup
64+
COPY --from=kani /usr/local/bin/* /usr/local/bin/
65+
COPY --from=kani /usr/local/rustup /usr/local/rustup
66+
# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
67+
COPY --from=kani /usr/local/kani /usr/local/kani
11568
# Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
11669
ENV RUSTUP_HOME=/usr/local/rustup
70+
# Point Kani at the system-wide installation
71+
ENV KANI_HOME=/usr/local/kani
11772
# Setup for codespaces
11873
COPY devenv-init.sh /usr/local/bin/
11974

‎devenv/Containerfile.debian‎

Lines changed: 18 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -26,71 +26,24 @@ apt -y update
2626
EORUN
2727

2828
FROM base as tools
29-
# renovate: datasource=github-releases depName=block/goose
30-
ARG gooseversion=v1.11.1
3129
# renovate: datasource=github-releases depName=bootc-dev/bcvk
3230
ARG bcvkversion=v0.9.0
3331
# renovate: datasource=github-releases depName=ossf/scorecard
3432
ARG scorecardversion=v5.1.1
35-
RUN <<EORUN
36-
set -xeuo pipefail
37-
arch=$(arch)
38-
39-
rm -vrf /usr/local/bin/*
40-
41-
# goose for local AI
42-
target=goose-${arch}-unknown-linux-gnu.tar.bz2
43-
/bin/time -f '%E %C' curl -fLO https://github.com/block/goose/releases/download/$gooseversion/$target
44-
tar xvjf $target
45-
mv goose /usr/local/bin/goose
46-
47-
# bcvk
48-
if test "${arch}" = x86_64; then
49-
td=$(mktemp -d)
50-
(
51-
cd $td
52-
target=bcvk-${arch}-unknown-linux-gnu
53-
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
54-
tar xvzf $target.tar.gz
55-
mv $target /usr/local/bin/bcvk
56-
)
57-
rm -rf $td
58-
else
59-
echo bcvk unavailable for $arch
60-
fi
61-
62-
# scorecard (OpenSSF security scanner)
63-
td=$(mktemp -d)
64-
(
65-
cd $td
66-
# Map arch to scorecard naming convention
67-
case "${arch}" in
68-
x86_64) scarch=amd64 ;;
69-
aarch64) scarch=arm64 ;;
70-
*) echo "scorecard unavailable for $arch"; exit 0 ;;
71-
esac
72-
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
73-
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
74-
tar xvzf $target
75-
mv scorecard /usr/local/bin/scorecard
76-
)
77-
rm -rf $td
78-
EORUN
33+
COPY fetch-tools.sh /run/src/
34+
RUN bcvkversion=$bcvkversion scorecardversion=$scorecardversion /run/src/fetch-tools.sh
7935

8036
FROM base as rust
81-
RUN <<EORUN
82-
set -xeuo pipefail
83-
# Setup rust; the idea here though is we install system-wide into /usr/local
84-
# as if it was packaged.
85-
export RUSTUP_HOME=/usr/local/rustup
86-
export CARGO_HOME=/usr/local/cargo
87-
# Install Rust system-wide
88-
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
89-
# Move binaries to /usr/local/bin (system-managed, root-owned)
90-
mv /usr/local/cargo/bin/* /usr/local/bin/
91-
# Nothing really left here
92-
rm -vrf /usr/local/cargo/bin
93-
EORUN
37+
COPY install-rust.sh /run/src/
38+
RUN /run/src/install-rust.sh
39+
40+
# Kani formal verification tool - requires rustup for toolchain management
41+
FROM rust as kani
42+
# renovate: datasource=crate depName=kani-verifier
43+
ARG kaniversion=0.67.0
44+
RUN apt-get update && apt-get install -y --no-install-recommends gcc libc6-dev && rm -rf /var/lib/apt/lists/*
45+
COPY install-kani.sh /run/src/
46+
RUN kaniversion=$kaniversion /run/src/install-kani.sh
9447

9548
# This builds the image.
9649
# Build this using `just devenv-build-debian` from the root of the repository.
@@ -108,10 +61,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
10861

10962
# Copy in the binaries from our tools container image
11063
COPY --from=tools /usr/local/bin/* /usr/local/bin/
111-
COPY --from=rust /usr/local/bin/* /usr/local/bin/
112-
COPY --from=rust /usr/local/rustup /usr/local/rustup
64+
COPY --from=kani /usr/local/bin/* /usr/local/bin/
65+
COPY --from=kani /usr/local/rustup /usr/local/rustup
66+
# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
67+
COPY --from=kani /usr/local/kani /usr/local/kani
11368
# Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
11469
ENV RUSTUP_HOME=/usr/local/rustup
70+
# Point Kani at the system-wide installation
71+
ENV KANI_HOME=/usr/local/kani
11572
# Setup for codespaces
11673
COPY devenv-init.sh /usr/local/bin/
11774

‎devenv/fetch-tools.sh‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#!/bin/bash
2+
# Fetch architecture-independent binary tools into /usr/local/bin
3+
# This script is shared between c10s and debian container builds.
4+
set -xeuo pipefail
5+
6+
# Required environment variables (passed as build ARGs)
7+
: "${bcvkversion:?bcvkversion is required}"
8+
: "${scorecardversion:?scorecardversion is required}"
9+
10+
arch=$(arch)
11+
12+
rm -vrf /usr/local/bin/*
13+
14+
# bcvk
15+
if test "${arch}" = x86_64; then
16+
td=$(mktemp -d)
17+
(
18+
cd $td
19+
target=bcvk-${arch}-unknown-linux-gnu
20+
/bin/time -f '%E %C' curl -fLO https://github.com/bootc-dev/bcvk/releases/download/$bcvkversion/${target}.tar.gz
21+
tar xvzf $target.tar.gz
22+
mv $target /usr/local/bin/bcvk
23+
)
24+
rm -rf $td
25+
else
26+
echo bcvk unavailable for $arch
27+
fi
28+
29+
# scorecard (OpenSSF security scanner)
30+
td=$(mktemp -d)
31+
(
32+
cd $td
33+
# Map arch to scorecard naming convention
34+
case "${arch}" in
35+
x86_64) scarch=amd64 ;;
36+
aarch64) scarch=arm64 ;;
37+
*) echo "scorecard unavailable for $arch"; exit 0 ;;
38+
esac
39+
target=scorecard_${scorecardversion#v}_linux_${scarch}.tar.gz
40+
/bin/time -f '%E %C' curl -fLO https://github.com/ossf/scorecard/releases/download/$scorecardversion/$target
41+
tar xvzf $target
42+
mv scorecard /usr/local/bin/scorecard
43+
)
44+
rm -rf $td

‎devenv/install-kani.sh‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#!/bin/bash
2+
# Install Kani formal verification tool
3+
# This script is shared between c10s and debian container builds.
4+
# Prerequisites: rustup must already be installed (via install-rust.sh)
5+
set -xeuo pipefail
6+
7+
# Required environment variable (passed as build ARG)
8+
: "${kaniversion:?kaniversion is required}"
9+
10+
export RUSTUP_HOME=/usr/local/rustup
11+
export CARGO_HOME=/usr/local/cargo
12+
export PATH="/usr/local/bin:$PATH"
13+
14+
# Install Kani to a system-wide location so all users can access it
15+
export KANI_HOME=/usr/local/kani
16+
17+
# Install kani-verifier
18+
/bin/time -f '%E %C' cargo install --locked kani-verifier --version $kaniversion
19+
20+
# Run kani setup - downloads bundle and installs required nightly toolchain
21+
/bin/time -f '%E %C' /usr/local/cargo/bin/cargo-kani setup
22+
23+
# Move kani binaries to /usr/local/bin, keep rustup symlink
24+
mv /usr/local/cargo/bin/cargo-kani /usr/local/cargo/bin/kani /usr/local/bin/

‎devenv/install-rust.sh‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#!/bin/bash
2+
# Install Rust system-wide into /usr/local
3+
# This script is shared between c10s and debian container builds.
4+
set -xeuo pipefail
5+
6+
export RUSTUP_HOME=/usr/local/rustup
7+
export CARGO_HOME=/usr/local/cargo
8+
9+
# Install Rust system-wide
10+
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
11+
12+
# Move binaries to /usr/local/bin (system-managed, root-owned)
13+
mv /usr/local/cargo/bin/* /usr/local/bin/
14+
15+
# Recreate bin directory with symlink to rustup - rustup's self-update check
16+
# looks for itself at $CARGO_HOME/bin/rustup
17+
mkdir -p /usr/local/cargo/bin
18+
ln -sf /usr/local/bin/rustup /usr/local/cargo/bin/rustup

0 commit comments

Comments
 (0)