From dae518d9e0a65f3fd232c29a1d2c165b5f161391 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 16 May 2025 19:58:01 -0700 Subject: [PATCH] Add setup scripts for Ubuntu 20.04 --- docs/src/build-from-source.md | 1 + scripts/setup/ubuntu-20.04 | 1 - scripts/setup/ubuntu-20.04/install_cbmc.sh | 32 +++++++++++++++ scripts/setup/ubuntu-20.04/install_deps.sh | 40 +++++++++++++++++++ .../setup/ubuntu-20.04/install_doc_deps.sh | 8 ++++ 5 files changed, 81 insertions(+), 1 deletion(-) delete mode 120000 scripts/setup/ubuntu-20.04 create mode 100755 scripts/setup/ubuntu-20.04/install_cbmc.sh create mode 100755 scripts/setup/ubuntu-20.04/install_deps.sh create mode 100755 scripts/setup/ubuntu-20.04/install_doc_deps.sh diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index c3d7ecfd4b9a..e7e43b07c6c8 100644 --- a/docs/src/build-from-source.md +++ b/docs/src/build-from-source.md @@ -27,6 +27,7 @@ is following our CI scripts: git clone https://github.com/model-checking/kani.git cd kani git submodule update --init + # For Ubuntu 20.04, use: `./scripts/setup/ubuntu-20.04/install_deps.sh` ./scripts/setup/ubuntu/install_deps.sh # If you haven't already (or from https://rustup.rs/): ./scripts/setup/install_rustup.sh diff --git a/scripts/setup/ubuntu-20.04 b/scripts/setup/ubuntu-20.04 deleted file mode 120000 index 7d13753d73e8..000000000000 --- a/scripts/setup/ubuntu-20.04 +++ /dev/null @@ -1 +0,0 @@ -ubuntu \ No newline at end of file diff --git a/scripts/setup/ubuntu-20.04/install_cbmc.sh b/scripts/setup/ubuntu-20.04/install_cbmc.sh new file mode 100755 index 000000000000..f9744f51f61f --- /dev/null +++ b/scripts/setup/ubuntu-20.04/install_cbmc.sh @@ -0,0 +1,32 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +# Source kani-dependencies to get CBMC_VERSION +source kani-dependencies + +if [ -z "${CBMC_VERSION:-}" ]; then + echo "$0: Error: CBMC_VERSION is not specified" + exit 1 +fi + +# Binaries are not released for Ubuntu 20.04, so build from source +WORK_DIR=$(mktemp -d) +git clone \ + --branch cbmc-${CBMC_VERSION} --depth 1 \ + https://github.com/diffblue/cbmc \ + "${WORK_DIR}" + +pushd "${WORK_DIR}" + +cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \ + -DCMAKE_C_COMPILER=gcc-10 -DCMAKE_CXX_COMPILER=g++-10 \ + -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \ + -DCMAKE_CXX_FLAGS=-Wno-error=register +cmake --build build -- -j$(nproc) +sudo make -C build install + +popd +rm -rf "${WORK_DIR}" diff --git a/scripts/setup/ubuntu-20.04/install_deps.sh b/scripts/setup/ubuntu-20.04/install_deps.sh new file mode 100755 index 000000000000..d9e272d18a84 --- /dev/null +++ b/scripts/setup/ubuntu-20.04/install_deps.sh @@ -0,0 +1,40 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +# Dependencies. +DEPS=( + bison + cmake + curl + flex + # CBMC needs g++-10 which doesn't come by default on Ubuntu 20.04 + g++-10 + gcc + git + gpg-agent + make + patch + wget + zlib1g + zlib1g-dev +) + +set -x + +# Github promises weekly build image updates, but recommends running +# `sudo apt-get update` before installing packages in case the `apt` +# index is stale. This prevents package installation failures. +# https://docs.github.com/en/actions/using-github-hosted-runners/customizing-github-hosted-runners#installing-software-on-ubuntu-runners +sudo apt-get --yes update + +sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}" + +# Get the directory containing this script +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + +${SCRIPT_DIR}/install_cbmc.sh +# The Kissat installation script is platform-independent, so is placed one level up +${SCRIPT_DIR}/../install_kissat.sh diff --git a/scripts/setup/ubuntu-20.04/install_doc_deps.sh b/scripts/setup/ubuntu-20.04/install_doc_deps.sh new file mode 100755 index 000000000000..e3f4dd2c0d74 --- /dev/null +++ b/scripts/setup/ubuntu-20.04/install_doc_deps.sh @@ -0,0 +1,8 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eux + +cargo install mdbook-graphviz +DEBIAN_FRONTEND=noninteractive sudo apt-get install --no-install-recommends --yes graphviz