# 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 static_libyices_dynamic. 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"]