Split the Rocq installation.

It should split the individual object size roughly in half.
Reduce image size by cleaning opam cache.
2026-01-01 11:53:59 -03:00 · 2026-01-01 10:36:26 -03:00 · 2025-12-28 19:12:41 -03:00
1 changed files with 14 additions and 1 deletions
--- a/15
+++ b/15
@ -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,16 @@ 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
+    && 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)
+# 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
Author	SHA1	Message	Date
Cesar Strauss	49076888de	Split the Rocq installation. It should split the individual object size roughly in half.	2026-01-01 11:53:59 -03:00
Cesar Strauss	17bd387064	Reduce image size by cleaning opam cache. Hopefully this sufficiently reduces the object size to allow it to upload to forgejo successfully.	2026-01-01 10:36:26 -03:00
Cesar Strauss	117d2cfcdf	Add Rocq to the installed dependencies.	2025-12-28 19:12:41 -03:00