# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

# Docker image for Kani GitHub Package release ubuntu-20-04.

FROM ubuntu:20.04
ENV DEBIAN_FRONTEND=noninteractive \
    DEBCONF_NONINTERACTIVE_SEEN=true \
    PATH="/root/.cargo/bin:${PATH}"
WORKDIR /tmp/kani
COPY ./kani-*-x86_64-unknown-linux-gnu.tar.gz ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
COPY ./target/package/kani-verifier-*[^e] ./kani-verifier

# Install Kani and dependencies. We will install the required
# toolchain by running an empty cargo command inside kani release
# directory. Rustup is purged for space.

RUN apt-get update && \
    apt-get install -y python3 python3-pip curl ctags && \
    curl -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain none && \
    (cd kani-verifier/; cargo) && \
    rustup default $(rustup toolchain list | awk '{ print $1 }') && \
    cargo install --path ./kani-verifier && \
    cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz && \
    apt-get clean && \
    rm -rf /tmp/kani/* /root/.rustup/toolchains/*/share