libre-chip/fayalite-deps
4
0
Fork 1
Code Issues Pull requests Projects Releases Packages 2 Wiki Activity Actions

Split the Rocq installation. #3

Merged
cesar merged 1 commit from cesar/fayalite-deps:add-rocq-dep into master 2026-01-01 14:56:26 +00:00
Conversation 0 Commits 1 Files changed 1 +4 -2
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
Containerfile
View file

@ -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