# -*- dockerfile-image-name: "ltpf-docker-image-2025" -*-
FROM ubuntu:24.04

USER root

# Avoid the need to provide answers

ARG DEBIAN_FRONTEND=noninteractive

# refresh package list

RUN apt update -y

# create unprivileged user

RUN apt install -y adduser

RUN adduser luser --disabled-password --gecos "Lambda User"

# install dependencies ...

# ... for opam

RUN apt install -y curl m4 gcc make unzip bubblewrap rsync git bzip2

# ... for Rocq

RUN apt-get install -y libgmp-dev pkg-config

# ... for Emacs (option A)

RUN apt install -y emacs emacs-common-non-dfsg

# ... for Rocq IDE (option B)

RUN apt-get install -y adwaita-icon-theme-full libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev

# install system-wide opam from the network

RUN curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh > /tmp/opam-install.sh
RUN sh -c "echo | sh /tmp/opam-install.sh"

# drop privileges

USER luser

# setup Rocq

RUN opam init --bare --yes --disable-sandboxing
RUN opam update -y
RUN opam switch create ltpf 4.14.2
RUN opam switch ltpf
RUN eval $(opam env)

RUN opam install -y merlin ocp-indent

RUN opam install -y user-setup

RUN opam pin add -y rocq-prover 9.0.0

RUN opam repo add rocq-released https://rocq-prover.org/opam/released

# option A : emacs setup

RUN curl -sL https://ltpf.gricad-pages.univ-grenoble-alpes.fr/commun/installation/ltpf_2020.emacs > /tmp/.emacs-luser
RUN cat /tmp/.emacs-luser >> ~/.emacs

RUN emacs --batch -l ~/.emacs --eval "(package-refresh-contents)"
RUN emacs --batch -l ~/.emacs --eval "(package-install 'tuareg)"         # OCaml mode
RUN emacs --batch -l ~/.emacs --eval "(package-install 'proof-general)"  # Coq mode

RUN emacs --batch -l ~/.emacs --eval "(package-install 'company)"        # optional
RUN emacs --batch -l ~/.emacs --eval "(package-install 'company-coq)"    # optional
RUN emacs --batch -l ~/.emacs --eval "(package-install 'auto-complete)"  # optional
RUN emacs --batch -l ~/.emacs --eval "(package-install 'merlin-eldoc)"   # optional
RUN emacs --batch -l ~/.emacs --eval "(package-install 'magit)"          # git mode (optional)

# option B : RocqIDE

RUN opam install -y rocqide

# option C : Ocaml/Rocq in vscode

RUN opam install -y vscoq-language-server
RUN opam install -y ocaml-lsp-server ocamlformat

# Finalize opam integration with editors

RUN opam user-setup install