# syntax=docker/dockerfile:1

FROM makarius/isabelle AS builder

USER root

# install dependencies
RUN \
    apt-get update -y && \
    apt-get install -y --no-install-recommends \
        curl \
        libnuma-dev \
        zlib1g-dev \
        libgmp-dev \
        libgmp10 \
        git \
        wget \
        lsb-release \
        software-properties-common \
        gnupg2 \
        apt-transport-https \
        gcc \
        autoconf \
        automake \
        build-essential \
 texlive-luatex \
 texlive-latex-base \
 texlive-plain-generic \
 texlive-latex-recommended \
 texlive-fonts-recommended

# install ghcup
RUN \
    curl https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup > /usr/bin/ghcup && \
    chmod +x /usr/bin/ghcup

ARG GHC=9.4.2
ARG CABAL=3.8.1.0

# install GHC and cabal
RUN \
    ghcup -v install ghc --isolate /usr/local --force ${GHC} && \
    ghcup -v install cabal --isolate /usr/local/bin --force ${CABAL}

USER isabelle

# set up Isabelle
ENV PATH="$PATH:/home/isabelle/Isabelle/bin"

# set up the AFP

RUN curl https://www.isa-afp.org/release/afp-current.tar.gz > afp-current.tar.gz && \
    tar xzf afp-current.tar.gz && \
    rm afp-current.tar.gz && \
    mv afp-* afp && \
    isabelle components -u /home/isabelle/afp/thys

WORKDIR /home/isabelle/secav-prover

USER root
RUN chown -R isabelle:isabelle /home/isabelle/secav-prover
USER isabelle

COPY --chown=isabelle  . .

RUN cabal update
RUN make
RUN cabal install secav-prover

FROM ubuntu:22.04

WORKDIR /root/
COPY --from=builder /home/isabelle/.cabal/bin/secav-prover ./

ENTRYPOINT ["./secav-prover"]