130 lines
4.3 KiB
Docker
130 lines
4.3 KiB
Docker
# MAIN: https://yices.csl.sri.com/
|
|
# REPO: https://github.com/SRI-CSL/yices2/
|
|
FROM localhost/notwa-util AS downloader
|
|
ENV YICES_COMMIT=708e65e260125a6196fad71ed4ebf4a41f4effc4
|
|
ENV YICES_SHA256=1f8087d01ab5d63821ce5e0e3ef12195bdede112c2f859f4733e9909d2ce38c8
|
|
# MAIN: https://gmplib.org/
|
|
# REPO: https://gmplib.org/repo/
|
|
ENV GMP_VERSION=6.2.1
|
|
ENV GMP_SHA256=fd4829912cddd12f84181c3451cc752be224643e87fac497b69edddadc49b4f2
|
|
# MAIN: http://fmv.jku.at/kissat/
|
|
# REPO: https://github.com/arminbiere/kissat
|
|
# FORK: https://github.com/BrunoDutertre/kissat
|
|
ENV KISSAT_COMMIT=315cd3227fd2321d29d10f7d8572011bf00174a5
|
|
ENV KISSAT_SHA256=031fca7efcb17c6f1921dd056052bd373de724e445fc2ed37bfdd5954148119f
|
|
|
|
RUN --mount=type=cache,id=common,target=/media/common,sharing=locked \
|
|
--mount=type=tmpfs,target=/tmp : \
|
|
&& cd /media/common \
|
|
&& name=yices \
|
|
&& export remote_fn="$YICES_COMMIT.tar.gz" \
|
|
&& export local_fn="$name-$remote_fn" \
|
|
&& export remote_url="https://github.com/SRI-CSL/yices2/archive/$remote_fn" \
|
|
&& export dest=/$name \
|
|
&& export sha256="$YICES_SHA256" \
|
|
&& acquire \
|
|
\
|
|
&& name=gmp \
|
|
&& export remote_fn="$name-$GMP_VERSION.tar.xz" \
|
|
&& export local_fn="$remote_fn" \
|
|
&& export remote_url="https://gmplib.org/download/gmp/$remote_fn" \
|
|
&& export dest=/$name \
|
|
&& export sha256="$GMP_SHA256" \
|
|
&& acquire \
|
|
\
|
|
&& name=kissat \
|
|
&& export remote_fn="$KISSAT_COMMIT.tar.gz" \
|
|
&& export local_fn="$name-$remote_fn" \
|
|
&& export remote_url="https://github.com/arminbiere/kissat/archive/$remote_fn" \
|
|
&& export dest=/$name \
|
|
&& export sha256="$KISSAT_SHA256" \
|
|
&& acquire \
|
|
;
|
|
|
|
FROM localhost/cosmo AS builder
|
|
|
|
RUN apk add --no-cache autoconf gperf make
|
|
|
|
RUN : \
|
|
&& cd /cosmopolitan \
|
|
&& tar zxf dist/headers.tar.gz \
|
|
;
|
|
COPY --chmod=0755 --from=localhost/notwa-util /usr/local/bin/cosmocc /usr/local/bin/quickconf /usr/bin/
|
|
|
|
COPY --from=downloader /kissat /kissat
|
|
WORKDIR /kissat
|
|
RUN : \
|
|
# the alarm function is located here: \
|
|
&& sed -i '/#include <unistd.h>/i\\#include <time.h>' src/application.c \
|
|
# completely override CFLAGS: \
|
|
&& sed -i '/passtocompiler -fpic/i\\CFLAGS=" -O2 -g -Wall"' configure \
|
|
# we don't need -static here because it's already part of cosmocc: \
|
|
&& CC=cosmocc ./configure \
|
|
;
|
|
|
|
RUN : \
|
|
&& make -j2 \
|
|
&& install -m 0644 -D -t /usr/local/lib build/libkissat.a \
|
|
&& install -m 0644 -D -t /usr/local/include -m644 src/kissat.h \
|
|
;
|
|
|
|
COPY --from=downloader /gmp /gmp
|
|
WORKDIR /gmp
|
|
RUN : \
|
|
&& CC=cosmocc CFLAGS="-O2 -g" \
|
|
# specify some generic old CPU for best compatibility/reproduciblity. \
|
|
# core2 introduced SSSE3, which cosmopolitan depends on, so use that: \
|
|
ac_cv_build='core2-pc-linux-gnu' \
|
|
ac_cv_host='core2-pc-linux-gnu' \
|
|
# this check takes ages for some reason, so just hardcode it here: \
|
|
gmp_cv_c_double_format='IEEE little endian' \
|
|
quickconf --disable-shared \
|
|
;
|
|
|
|
RUN : \
|
|
&& make -j2 \
|
|
&& make install \
|
|
;
|
|
|
|
COPY --from=downloader /yices /yices
|
|
WORKDIR /yices
|
|
RUN : \
|
|
# patch up some trivial incompatibilities with cosmopolitan: \
|
|
&& sed -i 's/\bdonothing\b/&_/g' src/context/context.c \
|
|
&& sed -i 's/\bhextoint\b/&_/g' src/terms/bv_constants.c src/terms/bv64_constants.c \
|
|
&& sed -i '/#include <unistd.h>/i\\#include <time.h>' src/utils/timeout.c \
|
|
# the static-lib target attempts to build a dynamic library. don't do that. \
|
|
&& sed -i 's/ $(static_libyices_dynamic)//g' src/Makefile \
|
|
\
|
|
&& autoconf \
|
|
&& CC=cosmocc \
|
|
CFLAGS="-O2 -g" \
|
|
CPPFLAGS="-I/usr/local/include -DHAVE_KISSAT" \
|
|
LDFLAGS="-L/usr/local/lib" \
|
|
LIBS="-lkissat" \
|
|
quickconf --prefix= \
|
|
;
|
|
|
|
RUN make -j2 static-dist
|
|
|
|
RUN : \
|
|
&& mv build/x86_64-pc-linux-gnu-release/static_dist dist \
|
|
&& cd dist/bin \
|
|
&& for bin in yices yices-sat yices-smt yices-smt2 \
|
|
;do : \
|
|
&& mv "$bin" "$bin.com.dbg" \
|
|
&& objcopy -S -O binary "$bin.com.dbg" "$bin.com" \
|
|
;done \
|
|
&& cd /kissat/build \
|
|
&& mv "kissat" "kissat.com.dbg" \
|
|
&& objcopy -S -O binary "kissat.com.dbg" "kissat.com" \
|
|
;
|
|
|
|
FROM scratch AS runner
|
|
COPY --chmod=0755 --from=localhost/notwa-util /usr/local/bin/busybox /bin/busybox
|
|
COPY --chmod=0755 --from=builder /cosmopolitan/dist/def/ape.elf /bin/ape
|
|
COPY --from=builder /yices/config.cache /yices/config.log /yices/config.status /var/local/
|
|
COPY --from=builder /yices/dist/bin /bin
|
|
COPY --chmod=0755 --from=builder /kissat/build/kissat.com /kissat/build/kissat.com.dbg /bin/
|
|
ENTRYPOINT ["/bin/ape", "/bin/yices.com"]
|