Bookworm fixes to enable making the formal docker

debian-bookworm/cvc/HDLC

@@ -34,6 +34,7 @@ makedepends=(
   python3-pyparsing
   python3-toml
   python3-venv
+  python3-pip
   openjdk-17-jre-headless
 )
 

debian-bookworm/formal.dockerfile

@@ -0,0 +1,109 @@
+# Authors:
+#   Unai Martinez-Corral
+#     <[email protected]>
+#     <[email protected]>
+#   Torsten Meissner
+#   Sverre Hamre
+#
+# Copyright Unai Martinez-Corral
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+# ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
+ARG REGISTRY='localhost/bookworm'
+
+#---
+
+# WORKAROUND: this is required because 'COPY --from' does not support ARGs
+FROM $REGISTRY/pkg/z3 AS pkg-z3
+FROM $REGISTRY/pkg/sby AS pkg-sby
+
+# FROM $REGISTRY/ghdl/yosys AS min
+FROM $REGISTRY/pkg/ghdl-yosys AS min
+
+COPY --from=pkg-z3 /z3 /
+COPY --from=pkg-sby /sby /
+
+RUN apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
+    python3 \
+    python3-pip \
+    python3-click \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+&& rm -rf /var/lib/apt/lists/* 
+# \
+#  && python3 -m pip install click --progress-bar off
+
+#---
+
+# WORKAROUND: this is required because 'COPY --from' does not support ARGs
+FROM $REGISTRY/pkg/yices2 AS pkg-yices2
+FROM $REGISTRY/pkg/boolector AS pkg-boolector
+FROM $REGISTRY/pkg/cvc AS pkg-cvc
+FROM $REGISTRY/pkg/pono AS pkg-pono
+
+FROM min AS latest
+
+COPY --from=pkg-yices2 /yices2 /
+COPY --from=pkg-boolector /boolector /
+COPY --from=pkg-cvc /cvc /
+COPY --from=pkg-pono /pono /
+
+RUN apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
+    libgmpxx4ldbl \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && rm -rf /var/lib/apt/lists/*
+
+#---
+
+# WORKAROUND: this is required because 'COPY --from' does not support ARGs# Create a francendebian with python2.7 from debian bulseye
+RUN curl -O http://ftp.debian.org/debian/pool/main/libf/libffi/libffi7_3.3-6_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/o/openssl/libssl1.1_1.1.1w-0+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-minimal_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7-minimal_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-stdlib_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7_2.7.18-8+deb11u1_amd64.deb
+# RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-dev_2.7.18-8+deb11u1_amd64.deb
+# RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7-dev_2.7.18-8+deb11u1_amd64.deb
+# RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7_2.7.18-8+deb11u1_amd64.deb
+
+RUN apt-get update -qq \
+&& apt-get -y install mime-support 
+
+RUN dpkg -i libffi7_3.3-6_amd64.deb 
+RUN dpkg -i libssl1.1_1.1.1w-0+deb11u1_amd64.deb 
+RUN dpkg -i libpython2.7-minimal_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i python2.7-minimal_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i libpython2.7-stdlib_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i python2.7_2.7.18-8+deb11u1_amd64.deb 
+# RUN dpkg -i libpython2.7_2.7.18-8+deb11u1_amd64.deb
+# RUN dpkg -i libpython2.7-dev_2.7.18-8+deb11u1_amd64.deb 
+# RUN dpkg -i python2.7-dev_2.7.18-8+deb11u1_amd64.deb 
+# End francendebian installs
+
+
+FROM $REGISTRY/pkg/superprove AS pkg-superprove
+
+FROM latest
+
+COPY --from=pkg-superprove /superprove /
+
+RUN apt-get update -qq \
+#  && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
+   #  python \
+   #  libpython2.7 \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && rm -rf /var/lib/apt/lists/*

debian-bookworm/ghdl-yosys-plugin.dockerfile

@@ -19,15 +19,18 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
+# ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
+ARG REGISTRY='localhost/bookworm'
 
 #---
 
-FROM $REGISTRY/yosys AS base
+FROM $REGISTRY/pkg/yosys AS base
 
 RUN apt-get update -qq \
  && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
     libgnat-12 \
+    gcc \
+    g++ \
  && apt-get autoclean && apt-get clean && apt-get -y autoremove \
  && rm -rf /var/lib/apt/lists
 

debian-bookworm/ghdl.dockerfile

@@ -23,7 +23,7 @@ ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
 
 #---
 
-FROM ghdl/pkg:bookworm-mcode AS build-mcode
+FROM docker.io/ghdl/pkg:bookworm-mcode AS build-mcode
 
 # TODO Build GHDL on $REGISTRY/build/build instead of picking ghdl/pkg:bookworm-mcode
 
@@ -35,7 +35,7 @@ COPY --from=build-mcode / /ghdl/usr/local/
 
 #---
 
-FROM ghdl/pkg:bookworm-llvm-14 AS build-llvm
+FROM docker.io/ghdl/pkg:bookworm-llvm-14 AS build-llvm
 
 # TODO Build GHDL on $REGISTRY/build/build instead of picking ghdl/pkg:bookworm-llvm-14
 
@@ -62,10 +62,12 @@ FROM base AS mcode
 COPY --from=build-mcode / /usr/local/
 
 #--
-
+   
 FROM base AS llvm
-
+   
 COPY --from=build-llvm / /usr/local/
+COPY --from=build-llvm / /ghdl/usr/local/
+COPY --from=build-mcode / /ghdl/usr/local/
 
 RUN apt-get update -qq \
  && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \

debian-bookworm/pono/Dockerfile

@@ -0,0 +1,48 @@
+# Authors:
+#   Unai Martinez-Corral
+#     <[email protected]>
+#     <[email protected]>
+#   Torsten Meissner
+#   Sverre Hamre
+#
+# Copyright Unai Martinez-Corral
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
+
+#---
+
+FROM $REGISTRY/build/build AS build
+
+RUN --mount=type=bind,target=/tmp/ctx . /tmp/ctx/HDLC \
+ && mkdir -p /usr/share/man/man1/ \
+ && apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install ${makedepends[@]} \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && update-ca-certificates \
+ && rm -rf /var/lib/apt/lists/*
+
+RUN --mount=type=bind,target=/tmp/ctx . /tmp/ctx/HDLC && build
+
+#---
+
+FROM scratch AS version
+COPY --from=build /tmp/hdlc.pono.version /
+
+#---
+
+FROM scratch
+COPY --from=build /opt/pono /pono

debian-bookworm/pono/HDLC

@@ -0,0 +1,53 @@
+# HDLC pono
+
+# Authors:
+#   Unai Martinez-Corral
+#     <[email protected]>
+#     <[email protected]>
+#   Torsten Meissner
+#   Sverre Hamre
+#
+# Copyright Unai Martinez-Corral
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+set -e
+
+makedepends=(
+  bison
+  cmake
+  flex
+  libbison-dev
+  libgmp-dev
+  python3-pyparsing
+  pkg-config
+  meson
+)
+
+
+build() {
+  git clone https://github.com/upscale-project/pono.git /tmp/pono
+  cd /tmp/pono
+  git describe --long --tags | sed 's/\([^-]*-g\)/r\1/;s/-/./g;s/^v//g' > /tmp/hdlc.pono.version
+  ./contrib/setup-smt-switch.sh
+  ./contrib/setup-btor2tools.sh
+  ./configure.sh
+  PREFIX=/usr/local
+  make -C build -j$(nproc) PREFIX="$PREFIX"
+  DESTDIR=/opt/pono
+  mkdir -p "${DESTDIR}${PREFIX}"/bin "${DESTDIR}${PREFIX}"/lib
+  cp build/pono "${DESTDIR}${PREFIX}"/bin/
+  cp build/libpono.so "${DESTDIR}${PREFIX}"/lib/
+}

debian-bookworm/superprove/Dockerfile

@@ -0,0 +1,75 @@
+# Authors:
+#   Unai Martinez-Corral
+#     <[email protected]>
+#     <[email protected]>
+#   Torsten Meissner
+#   Sverre Hamre
+#
+# Copyright Unai Martinez-Corral
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+#
+# SPDX-License-Identifier: Apache-2.0
+
+ARG REGISTRY='gcr.io/hdl-containers/debian/bookworm'
+
+#---
+
+FROM $REGISTRY/build/build AS build
+
+# Create a francendebian with python2.7 from debian bulseye
+RUN curl -O http://ftp.debian.org/debian/pool/main/libf/libffi/libffi7_3.3-6_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/o/openssl/libssl1.1_1.1.1w-0+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-minimal_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7-minimal_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-stdlib_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7-dev_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/python2.7-dev_2.7.18-8+deb11u1_amd64.deb
+RUN curl -O http://ftp.debian.org/debian/pool/main/p/python2.7/libpython2.7_2.7.18-8+deb11u1_amd64.deb
+
+RUN apt-get update -qq \
+&& apt-get -y install mime-support libexpat1-dev
+
+RUN dpkg -i libffi7_3.3-6_amd64.deb 
+RUN dpkg -i libssl1.1_1.1.1w-0+deb11u1_amd64.deb 
+RUN dpkg -i libpython2.7-minimal_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i python2.7-minimal_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i libpython2.7-stdlib_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i python2.7_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i libpython2.7_2.7.18-8+deb11u1_amd64.deb
+RUN dpkg -i libpython2.7-dev_2.7.18-8+deb11u1_amd64.deb 
+RUN dpkg -i python2.7-dev_2.7.18-8+deb11u1_amd64.deb 
+# End francendebian installs
+
+
+RUN --mount=type=bind,target=/tmp/ctx . /tmp/ctx/HDLC \
+ && apt-get update -qq \
+ && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends ${makedepends[@]} \
+ && apt-get autoclean && apt-get clean && apt-get -y autoremove \
+ && update-ca-certificates \
+ && rm -rf /var/lib/apt/lists/* 
+ #\
+ #&& prepare
+
+RUN --mount=type=bind,target=/tmp/ctx . /tmp/ctx/HDLC && build
+
+#---
+
+FROM scratch AS version
+COPY --from=build /tmp/hdlc.superprove.version /
+
+#---
+
+FROM scratch
+COPY --from=build /opt/superprove /superprove