Skip to content

Commit

Permalink
cvc5: use mainline cvc5 (#25)
Browse files Browse the repository at this point in the history
  • Loading branch information
sorawee committed Mar 13, 2024
1 parent 783b4e5 commit d88a659
Show file tree
Hide file tree
Showing 4 changed files with 39 additions and 34 deletions.
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: Docker Base Image
name: Docker Base Image Push

on: workflow_dispatch

Expand Down
22 changes: 22 additions & 0 deletions .github/workflows/docker-base-test.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
name: Docker Base Image Test

on:
pull_request:
paths:
resources/Dockerfile@base

jobs:
build-base-docker:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v2
- name: Build Docker
uses: docker/build-push-action@v3
with:
context: .
push: false
file: resources/Dockerfile@base
platforms: linux/amd64
2 changes: 2 additions & 0 deletions changelogs/unreleased/23-11-21-cvc5-upgrade.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
changed:
- Upgraded cvc5 to version 1.0.9-dev.145.de62429fa
47 changes: 14 additions & 33 deletions resources/Dockerfile@base
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,20 @@ RUN set -x && \
jq \
time

# fetch cvc5-ff
RUN pip install tomli scikit-build Cython && \
git clone https://github.com/cvc5/cvc5.git --single-branch && \
cd cvc5 && \
git checkout de62429

# compile and install cvc5-ff
RUN cd ./cvc5/ && \
./configure.sh --cocoa --auto-download --python-bindings --ninja && \
cd ./build/ && \
cmake --build . && \
cmake --install . && \
cd ../.. && rm -r ./cvc5

# racket and rosette and other racket packages
ARG DEBIAN_FRONTEND=noninteractive
RUN add-apt-repository -y ppa:plt/racket && \
Expand Down Expand Up @@ -52,37 +66,4 @@ RUN wget https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3-4.11.0-x6
cp z3-4.11.0-x64-glibc-2.31/bin/z3 /bin/ && \
rm -r z3-4.11.0-x64-glibc-2.31/

# install libpoly
RUN git clone https://github.com/SRI-CSL/libpoly.git && \
cd ./libpoly/ && \
cd ./build/ && \
cmake .. -GNinja -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/usr/local && \
cmake --build . && \
cmake --install . && \
cd ../../ && rm -r ./libpoly

# fetch cvc5-ff
RUN pip install toml && \
git clone https://github.com/alex-ozdemir/CVC4.git -b ff --single-branch && \
cd ./CVC4 && \
git checkout ddcecc5

# compile and install CoCoALib with patch from cvc5-ff
RUN wget https://cocoa.dima.unige.it/cocoa/cocoalib/tgz/CoCoALib-0.99800.tgz && \
tar -xvzf CoCoALib-0.99800.tgz &&\
patch -s -p1 -d ./CoCoALib-0.99800 < ./CVC4/cmake/deps-utils/CoCoALib-0.99800-trace.patch && \
cd CoCoALib-0.99800/ && \
./configure && \
make && \
make install && \
cd .. && rm -r ./CoCoALib-0.99800

# compile and install cvc5-ff
RUN cd ./CVC4/ && \
./configure.sh --cocoa --auto-download --ninja && \
cd ./build/ && \
cmake --build . && \
cmake --install . && \
cd ../.. && rm -r ./CVC4

CMD [ "/bin/bash" ]

0 comments on commit d88a659

Please sign in to comment.