#!/bin/not_a_shell_script

# This is not a Shel script: please execute manually and read outputs before proceeding !
exit 42 # Read previous line again ...

# Intended for recent Debian/Ubuntu using apt (tested only for Ubuntu 24.04),
# Changes might be needed for other linux distributions

# ---------------------------------------------------------------------------
# CHAPTER 1 : system-wide installation (as root via sudo)

# refresh package list

sudo apt update -y

# install dependencies ...

# ... for opam

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

# ... for Rocq

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

# ... for Emacs (option A)

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

# ... for Rocq IDE (option B)

sudo 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

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

# ---------------------------------------------------------------------------
# CHAPTER 2 : user-local installation (no sudo / not as root)

# setup OCaml and Rocq

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

opam install -y merlin ocp-indent
opam install -y user-setup
opam pin add -y rocq-prover 9.0.0  # about 10 minutes to compile + install stdlib

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

# option A : emacs setup (a few seconds)

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

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

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

# for windows-like shortcuts in emacs, cf https://www.emacswiki.org/emacs/CuaMode

# option B : RocqIDE (about 2 min)

opam install -y rocqide

# option C : Ocaml/Rocq in vscode

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

# Finalize opam integration with editors

opam user-setup install