Skip to content

devenv: Deduplicate kani setup and devcontainer configs #145

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
cgwalters merged 1 commit into from
Mar 23, 2026
Merged

devenv: Deduplicate kani setup and devcontainer configs #145

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/build-devcontainer.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ on:
pull_request:
paths:
- 'devenv/**'
- 'common/.devcontainer/**'
- '.github/workflows/build-devcontainer.yml'

env:
Expand Down
23 changes: 22 additions & 1 deletion Justfile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,26 @@
# Validate devcontainer.json syntax
# Generate per-OS devcontainer.json from the default (debian) template
devcontainer-generate:
#!/bin/bash
set -euo pipefail
template=common/.devcontainer/devcontainer.json
for os in debian ubuntu; do
mkdir -p "common/.devcontainer/${os}"
sed -e "s/devenv-debian/devenv-${os}/g" "$template" > "common/.devcontainer/${os}/devcontainer.json"
done

# Validate devcontainer.json syntax and that per-OS configs are in sync
devcontainer-validate:
Copy link
Copy Markdown
Contributor

@cgwalters cgwalters Mar 19, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But nothing is invoking this in CI?

Copy link
Copy Markdown
Contributor

@cgwalters cgwalters Mar 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You marked this as resolved but it seems unchanged? What I meant was: if someone modifies one of the container files directly, it won't fail CI but it should

Copy link
Copy Markdown
Contributor Author

@henrywang henrywang Mar 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The just devcontainer-validate is already called in the build-devcontainer.yml workflow. I added 'common/.devcontainer/**' in line 10 to trigger validation when devcontainer configs change.

Copy link
Copy Markdown
Contributor

@cgwalters cgwalters Mar 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Got it sorry! I was confused when reading the diff, I missed that the validate line didn't change and that meant it was already called.

#!/bin/bash
set -euo pipefail
template=common/.devcontainer/devcontainer.json
for os in debian ubuntu; do
if ! diff -u "common/.devcontainer/${os}/devcontainer.json" <(sed "s/devenv-debian/devenv-${os}/g" "$template"); then
echo "ERROR: common/.devcontainer/${os}/devcontainer.json is out of sync with template"
echo "Run 'just devcontainer-generate' to fix"
exit 1
fi
done
echo "All devcontainer configs are in sync"
npx --yes @devcontainers/cli read-configuration --workspace-folder .

# Build devenv Debian image with local tag
Expand Down
1 change: 0 additions & 1 deletion devenv/Containerfile.c10s
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# These aren't packages, just low-dependency binaries dropped in /usr/local/bin
# so we can fetch them independently in a separate build.
ARG base=quay.io/centos/centos:stream10
FROM $base as base

Check warning on line 4 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, amd64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

Check warning on line 4 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, arm64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/
# Life is too short to care about dash
RUN ln -sfr /bin/bash /bin/sh
RUN <<EORUN
Expand All @@ -25,24 +25,23 @@
dnf -y makecache
EORUN

FROM base as tools

Check warning on line 28 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, amd64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

Check warning on line 28 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, arm64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/
# renovate: datasource=github-releases depName=astral-sh/uv
ARG uvversion=0.10.11
COPY fetch-tools.py tool-versions.txt install-uv.sh /run/src/
RUN /run/src/fetch-tools.py
RUN uvversion=$uvversion /run/src/install-uv.sh

FROM base as rust

Check warning on line 35 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, amd64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

Check warning on line 35 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, arm64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/
# renovate: datasource=custom.rust-nightly depName=rust-nightly versioning=rust-release-channel
ARG rust_nightly=nightly-2026-03-17
COPY install-rust.sh /run/src/
RUN rust_nightly=$rust_nightly /run/src/install-rust.sh

# Kani formal verification tool - requires rustup for toolchain management
FROM rust as kani

Check warning on line 42 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, amd64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

Check warning on line 42 in devenv/Containerfile.c10s

View workflow job for this annotation

GitHub Actions / build (c10s, arm64)

The 'as' keyword should match the case of the 'from' keyword 

FromAsCasing: 'as' and 'FROM' keywords' casing do not match
More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/
# renovate: datasource=crate depName=kani-verifier
ARG kaniversion=0.67.0
RUN dnf install -y gcc && dnf clean all
COPY install-kani.sh /run/src/
RUN kaniversion=$kaniversion /run/src/install-kani.sh

Expand Down
1 change: 0 additions & 1 deletion devenv/Containerfile.debian
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ RUN rust_nightly=$rust_nightly /run/src/install-rust.sh
FROM rust AS kani
# renovate: datasource=crate depName=kani-verifier
ARG kaniversion=0.67.0
RUN apt-get update && apt-get install -y --no-install-recommends gcc libc6-dev && rm -rf /var/lib/apt/lists/*
COPY install-kani.sh /run/src/
RUN kaniversion=$kaniversion /run/src/install-kani.sh

Expand Down
1 change: 0 additions & 1 deletion devenv/Containerfile.ubuntu
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ RUN rust_nightly=$rust_nightly /run/src/install-rust.sh
FROM rust AS kani
# renovate: datasource=crate depName=kani-verifier
ARG kaniversion=0.67.0
RUN apt-get update && apt-get install -y --no-install-recommends gcc libc6-dev && rm -rf /var/lib/apt/lists/*
COPY install-kani.sh /run/src/
RUN kaniversion=$kaniversion /run/src/install-kani.sh

Expand Down
12 changes: 11 additions & 1 deletion devenv/install-kani.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,22 @@
#!/bin/bash
# Install Kani formal verification tool
# This script is shared between c10s and debian container builds.
# This script is shared between c10s, debian, and ubuntu container builds.
# Prerequisites: rustup must already be installed (via install-rust.sh)
set -xeuo pipefail

# Required environment variable (passed as build ARG)
: "${kaniversion:?kaniversion is required}"

# Install gcc (required to compile Kani's C stubs)
if command -v dnf >/dev/null; then
dnf install -y gcc && dnf clean all
elif command -v apt-get >/dev/null; then
apt-get update && apt-get install -y --no-install-recommends gcc libc6-dev && rm -rf /var/lib/apt/lists/*
else
echo "error: unsupported package manager" >&2
exit 1
fi

export RUSTUP_HOME=/usr/local/rustup
export CARGO_HOME=/usr/local/cargo
export PATH="/usr/local/bin:$PATH"
Expand Down
Loading