# Maintainer: Baptiste Jonglez <baptiste--aur at jonglez dot org>
# Contributor: acieroid
# Contributor: spider-mario <spidermario@free.fr>
# Contributor: Thomas Dziedzic < gostrc at gmail >
# Contributor: George Giorgidze <giorgidze@gmail.com>
# Contributor: William J. Bowman <bluephoenix47@gmail.com>

pkgname=('coq' 'coqide' 'coq-doc')
pkgver=8.9.1
pkgrel=3
pkgdesc='Formal proof management system'
arch=('x86_64')
url='https://coq.inria.fr/'
license=('GPL')
groups=('coq')
options=('!emptydirs')
depends=('ocaml' 'camlp5' 'ocaml-num' 'gtk2' 'gtksourceview2')
makedepends=('ocaml-findlib'
             'lablgtk2' 'gendesk' # coqide
             'texlive-bin' 'texlive-latexextra' 'texlive-pictures' # coq-doc
             'texlive-fontsextra' 'texlive-science'
             'fig2dev' 'imagemagick' 'hevea' 'ghostscript'
             'python' 'python-sphinx' 'python-sphinx_rtd_theme' 'python-pexpect'
             'python-beautifulsoup4' 'python-sphinxcontrib-bibtex' 'python-antlr4')
source=("coq-${pkgver}.tar.gz::https://github.com/coq/coq/archive/V${pkgver}.tar.gz"
"ocaml408_compat.patch")
sha512sums=('66344f801b955d1b6daf3ab1d704551070c95cf9032ae74f15fb33f7ec313812b3e05c0ec277a2eb448e3fdfd9721df06d36612e2fb4928b6530d70147f1d983'
'df50beaf50e8ed6c208682327634ba0c656d041598d9a81d762ba07bba01336b769defc9deabe0e37c66deca3bce8c418c16da26c084564c2147e55b646508f5')

prepare() {
  gendesk -f -n --pkgname "coqide" \
    --name "CoqIDE Proof Assistant" \
    --pkgdesc "Graphical interface for the Coq proof assistant" \
    --categories "Development;Science;Math;IDE;GTK"
  cd "$srcdir/coq-$pkgver"
  patch -p1 -i "${srcdir}/ocaml408_compat.patch"
}

build() {
  cd "$srcdir/coq-$pkgver"

  ./configure \
    -prefix '/usr' \
    -mandir '/usr/share/man' \
    -configdir '/etc/xdg/coq/' \
    -coqide opt \
    -with-doc yes

  make world
}

package_coq() {
  depends=('ocaml' 'camlp5')
  optdepends=('coqide: graphical Coq IDE'
              'coq-doc: offline documentation'
              'coin-or-csdp: for psatz plugin')
  # coq-nox was the old name for coq without coqide
  replaces=('coq-nox')
  conflicts=('coq-nox')

  cd "$srcdir/coq-$pkgver"

  # The second target is needed to install coqidetop.cmxs (needed for some
  # frontend other than coqide, for instance coquille)
  make COQINSTALLPREFIX="$pkgdir" install-coq install-ide-toploop install-meta
  rm -f "${pkgdir}/usr/share/man/man1/coqide.1"
  # Workaround for FS#58203
  mkdir -p "$pkgdir/usr/lib/ocaml/"
  ln -s /usr/lib/coq "$pkgdir/usr/lib/ocaml/coq"
}

package_coqide() {
  pkgdesc="GTK-based graphical interface for the Coq proof assistant"
  depends=('coq' 'ocaml' 'camlp5' 'gtk2' 'gtksourceview2')

  cd "$srcdir/coq-$pkgver"

  mkdir -p "${pkgdir}/usr/bin"
  make COQINSTALLPREFIX="$pkgdir" install-coqide
  install -D -m 644 -t "${pkgdir}/usr/share/man/man1/" man/coqide.1

  # Remove toploop files installed by "install-ide-toploop" in the main package
  rm -f "${pkgdir}/usr/lib/coq/toploop"/coqidetop.{cma,cmxs}
  rm -f "${pkgdir}/usr/bin"/coqidetop{,.opt}
  # In coq 8.7 this file is installed both by install-coq and install-coqide, remove the duplicate.
  rm -f "${pkgdir}/usr/lib/coq/vernac/topfmt.cmi"

  # Desktop file generated by gendesk
  install -D -m 644 "${srcdir}/${pkgname}.desktop" "${pkgdir}/usr/share/applications/${pkgname}.desktop"
  install -D -m 644 ide/coq.png "${pkgdir}/usr/share/pixmaps/${pkgname}.png"
}

package_coq-doc() {
  pkgdesc="HTML and PDF documentation for the Coq proof assistant"
  depends=()

  cd "$srcdir/coq-$pkgver"

  make COQINSTALLPREFIX="$pkgdir" install-doc
}
