# Maintainer: Konstantin Gizdov <arch at kge dot pw>
# Contributor: 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>

pkgbase=coq
pkgname=("${pkgbase}" "${pkgbase}ide" "${pkgbase}-doc")
pkgver=8.16.1
pkgrel=1
pkgdesc='Formal proof management system'
arch=('x86_64')
url='https://coq.inria.fr/'
license=('GPL')
groups=('coq')
options=('!emptydirs' '!strip' 'staticlibs')
depends=('ocaml>=4.14.0' 'ocaml-findlib')
makedepends=('ocaml-num' 'ocaml-zarith' 'gtk3' 'gtksourceview3' 'dune' 'git'
             'lablgtk3' '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' 'antlr4' 'python-antlr4')
source=("coq-${pkgver}.tar.gz::https://github.com/coq/coq/archive/V${pkgver}.tar.gz")
sha512sums=('e9c82f1a180c2e3946628e8e039999a1841397a5b4cd77f158de69876fa43b5c0f61ce76c510cc2b2f646a489110aea59da452b88ddd7850d1eab4105f1382f5')

build() {
  # generate a desktop file
  cd "${srcdir}"
  gendesk -f -n --pkgname "${pkgbase}ide" \
    --name "CoqIDE Proof Assistant" \
    --pkgdesc "Graphical interface for the Coq proof assistant" \
    --categories "Development;Science;Math;IDE;GTK"

  # build package
  cd "${srcdir}/${pkgbase}-${pkgver}"

  make clean
  ./configure \
    -prefix '/usr' \
    -mandir '/usr/share/man' \
    -configdir '/etc/xdg/coq/' \
    -nomacintegration \
    -warn-error no \
    -coqide opt \
    -with-doc yes
  # https://github.com/antlr/antlr4/issues/3753
  make -C doc/tools/coqrst/notations
  MAKE_TARGETS="coq coqide revision refman-html doc-stdlib" # refman-pdf is currently broken
  # https://github.com/coq/coq/issues/12332
  OCAMLPATH=/usr/lib/ocaml CAML_LD_LIBRARY_PATH=/usr/lib/ocaml/zarith/ SPHINXWARNERROR=0 make $MAKE_TARGETS
}

package_coq() {
  optdepends=('coqide: graphical Coq IDE'
              'coq-doc: offline documentation'
              'coin-or-csdp: for psatz plugin'
              'python-argparse: needed by some coq tools (e.g. TimeFileMaker)')
  # coq-nox was the old name for coq without coqide
  replaces=('coq-nox')
  conflicts=('coq-nox')

  cd "${srcdir}/${pkgbase}-${pkgver}"

  # fix intermittent bug with folder creation
  install -d "${pkgdir}/usr/bin"
  install -d "${pkgdir}/usr/lib/coq"
  install -d "${pkgdir}/usr/lib/coq-core"
  # Workaround for FS#58203
  install -d "${pkgdir}/usr/lib/ocaml"
  ln -s /usr/lib/coq "${pkgdir}/usr/lib/ocaml/coq"
  ln -s /usr/lib/coq-core "${pkgdir}/usr/lib/ocaml/coq-core"
  ln -s /usr/lib/coqide-server "${pkgdir}/usr/lib/ocaml/coqide-server"

  # The second target is needed to install coqidetop.cmxs (needed for some
  # frontend other than coqide, for instance coquille)
  make DESTDIR="${pkgdir}" install-coq install-coqide
  rm -f "${pkgdir}/usr/share/man/man1/coqide.1"
  rm -rf "${pkgdir}"/usr/{bin,doc,lib,share/doc}/coqide
}

package_coqide() {
  pkgdesc="GTK-based graphical interface for the Coq proof assistant"
  depends+=("${pkgbase}" 'gtk3' 'gtksourceview3')

  cd "${srcdir}/${pkgbase}-${pkgver}"

  mkdir -p "${pkgdir}/usr/bin"
  make DESTDIR="${pkgdir}" install-coqide
  install -D -m 644 -t "${pkgdir}/usr/share/man/man1/" man/coqide.1
  # Workaround for FS#58203
  install -d "${pkgdir}/usr/lib/ocaml"
  ln -s /usr/lib/coqide "${pkgdir}/usr/lib/ocaml/coqide"

  # 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"
  rm -rf "${pkgdir}/usr/share/coq"

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

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

  cd "${srcdir}/${pkgbase}-${pkgver}"

  make DESTDIR="${pkgdir}" install-doc
}