# MAIN: https://yices.csl.sri.com/
# REPO: https://github.com/SRI-CSL/yices2/
FROM localhost/notwa-util AS downloader
ARG YICES_COMMIT=316ab8c2ba723231c12efec9948090718bbc8ce5
ARG YICES_SHA256=c2e0a85069ce8eb5029830190d6d282dab36cc28ca872682f9a619c089deff2e
# MAIN: https://gmplib.org/
# REPO: https://gmplib.org/repo/
ARG GMP_VERSION=6.2.1
ARG GMP_SHA256=fd4829912cddd12f84181c3451cc752be224643e87fac497b69edddadc49b4f2
# MAIN: http://fmv.jku.at/kissat/
# REPO: https://github.com/arminbiere/kissat
# FORK: https://github.com/BrunoDutertre/kissat
ARG KISSAT_COMMIT=315cd3227fd2321d29d10f7d8572011bf00174a5
ARG KISSAT_SHA256=031fca7efcb17c6f1921dd056052bd373de724e445fc2ed37bfdd5954148119f

RUN --mount=type=cache,id=common,target=/media/common,sharing=locked \
    --mount=type=tmpfs,target=/tmp : \
 && acquire from=github repo=SRI-CSL/yices2 dest=/yices env=YICES \
\
 && name=gmp \
 && 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 \
\
 && acquire from=github repo=arminbiere/kissat dest=/kissat env=KISSAT \
;

FROM localhost/cosmo AS builder

RUN apk add --no-cache autoconf gperf

RUN : \
 && cd /cosmopolitan \
 && tar zxf dist/headers.tar.gz \
 && install -m0755 bin/make.com /usr/bin/make \
 && bin/ape bin/assimilate.com /usr/bin/make \
;
COPY --chmod=0755 --from=localhost/notwa-util /nu/cosmocc /nu/quickconf /nu/shed /usr/bin/

COPY --from=downloader /kissat /kissat
WORKDIR /kissat
RUN : \
# the alarm function is located here: \
 && shed src/application.c '/#include <unistd.h>/i\\#include <time.h>' \
# completely override CFLAGS: \
 && shed configure '/passtocompiler -fpic/i\\CFLAGS=" -O2 -g -Wall"' \
# 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: \
 && shed src/context/context.c 's/\bdonothing\b/&_/g' \
 && shed src/terms/bv_constants.c 's/\bhextoint\b/&_/g' \
 && shed src/terms/bv64_constants.c 's/\bhextoint\b/&_/g' \
 && shed src/utils/timeout.c '/#include <unistd.h>/i\\#include <time.h>' \
# the static-lib target attempts to build a dynamic library. don't do that. \
 && shed src/Makefile 's/ $(static_libyices_dynamic)//g' \
\
 && 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 /nu/busybox /bin/busybox
COPY --chmod=0755 --from=builder /cosmopolitan/bin/ape /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"]