# Based on: https://github.com/rsasse/tamarin-prover-docker/blob/0d1b7fa10943fbae731772ad15f6a919f61a7dcf/Dockerfile

FROM ubuntu:latest AS base

RUN set -xe \
	&& apt-get update \
	&& apt-get upgrade -y
        
FROM base AS dependencies

ENV VERSION 1.6.0

ENV MAUDE_URL http://maude.cs.illinois.edu/w/images/5/5d/Maude-2.7.1-linux.zip
# ENV MAUDE_URL https://maude.cs.illinois.edu/w/images/3/38/Maude-3.1-linux.zip
# ENV MAUDE_URL http://maude.cs.illinois.edu/w/images/2/27/Maude-3.0%2Byices2-linux.zip
# maude-Yices2.linux64
# ENV MAUDE_URL http://maude.cs.illinois.edu/w/images/7/73/Maude-3.0%2Bcvc4-linux.zip
# maude-CVC4.linux64

RUN set -xe \
	&& mkdir -p /dependencies \
	&& apt-get install -y curl zip wget \
	&& curl -q -s -S -L --create-dirs -o maude.zip $MAUDE_URL \
	&& unzip maude.zip -d /dependencies \
	&& mv /dependencies/maude.linux64 /dependencies/maude \
	#&& mv /dependencies/maude-Yices2.linux64 /dependencies/maude \
	#&& mv /dependencies/maude-CVC4.linux64 /dependencies/maude \
	&& curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin-prover/tamarin-prover/releases/download/$VERSION/tamarin-prover-$VERSION-linux64-ubuntu.tar.gz \
	&& tar -x -C /dependencies -f tamarin.tar.gz \
	&& chmod -R +x /dependencies

FROM base AS runtime

VOLUME /workspace

EXPOSE 3001

COPY --from=dependencies /dependencies /usr/local/bin

RUN set -xe \
	&& addgroup tamarin \
	&& adduser --disabled-password --gecos '' --ingroup tamarin tamarin \
	&& apt-get install -y graphviz libtinfo5 python3 \
	&& apt-get clean

#ENV LANG en_US.UTF-8  
#ENV LANGUAGE en_US:en  
ENV LC_ALL C.UTF-8
	
USER tamarin

WORKDIR /workspace

ENTRYPOINT ["tamarin-prover"]

CMD ["interactive", "."]