From 117d2cfcdfb84efbd3cfe1255e04b08b273c0a6d Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 28 Dec 2025 19:12:41 -0300 Subject: [PATCH 1/3] Add Rocq to the installed dependencies. --- Containerfile | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Containerfile b/Containerfile index 5e96ddb..26d191e 100644 --- a/Containerfile +++ b/Containerfile @@ -27,6 +27,7 @@ RUN apt-get -qq update && apt-get -qq install \ libffi-dev \ libreadline-dev \ lld \ + opam \ openfpgaloader \ pkg-config \ python3 \ @@ -113,4 +114,13 @@ RUN git clone --depth=1 --recursive --branch=z3-4.13.3 https://git.libre-chip.or && cd build \ && make -j"$(nproc)" \ && make install \ - && rm -rf /build \ No newline at end of file + && rm -rf /build + +# Install Rocq. Based on: +# https://rocq-prover.org/docs/using-opam#installing-rocq +# https://github.com/rocq-community/docker-base/blob/71a2b78f4faf9c1dc658e1c4bf920dff2257787f/base/rocq-single/Dockerfile#L87 (BSD license) +# https://gitlab.com/rocq-community/docker-rocq/-/blob/c4507ab5c137227700dac7e35fb5c0747fcd272f/rocq/stable/Dockerfile (MIT license) +RUN opam init --auto-setup --yes --disable-sandboxing \ + && eval $(opam env) \ + && opam pin -y add rocq-prover 9.0.0 +ENV PATH=/root/.opam/default/bin:$PATH From 17bd38706483cef0f353d2c1bc9a7287729cba14 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Thu, 1 Jan 2026 10:36:26 -0300 Subject: [PATCH 2/3] Reduce image size by cleaning opam cache. Hopefully this sufficiently reduces the object size to allow it to upload to forgejo successfully. --- Containerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Containerfile b/Containerfile index 26d191e..766ebb2 100644 --- a/Containerfile +++ b/Containerfile @@ -122,5 +122,6 @@ RUN git clone --depth=1 --recursive --branch=z3-4.13.3 https://git.libre-chip.or # https://gitlab.com/rocq-community/docker-rocq/-/blob/c4507ab5c137227700dac7e35fb5c0747fcd272f/rocq/stable/Dockerfile (MIT license) RUN opam init --auto-setup --yes --disable-sandboxing \ && eval $(opam env) \ - && opam pin -y add rocq-prover 9.0.0 + && opam pin -y add rocq-prover 9.0.0 \ + && opam clean -a -r -c -s --logs ENV PATH=/root/.opam/default/bin:$PATH From 49076888de2f2d06a4360a1c87766860d927c925 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Thu, 1 Jan 2026 11:53:59 -0300 Subject: [PATCH 3/3] Split the Rocq installation. It should split the individual object size roughly in half. --- Containerfile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Containerfile b/Containerfile index 766ebb2..ccf0ea0 100644 --- a/Containerfile +++ b/Containerfile @@ -120,8 +120,10 @@ RUN git clone --depth=1 --recursive --branch=z3-4.13.3 https://git.libre-chip.or # https://rocq-prover.org/docs/using-opam#installing-rocq # https://github.com/rocq-community/docker-base/blob/71a2b78f4faf9c1dc658e1c4bf920dff2257787f/base/rocq-single/Dockerfile#L87 (BSD license) # https://gitlab.com/rocq-community/docker-rocq/-/blob/c4507ab5c137227700dac7e35fb5c0747fcd272f/rocq/stable/Dockerfile (MIT license) -RUN opam init --auto-setup --yes --disable-sandboxing \ - && eval $(opam env) \ +# initialize an "opam switch" +RUN opam init --auto-setup --yes --disable-sandboxing +# install Rocq inside the default switch +RUN eval $(opam env) \ && opam pin -y add rocq-prover 9.0.0 \ && opam clean -a -r -c -s --logs ENV PATH=/root/.opam/default/bin:$PATH