sci-mathematics/coq/coq-8.20.0.ebuild

   1 # Copyright 1999-2024 Gentoo Authors
   2 # Distributed under the terms of the GNU General Public License v2
   3
   4 EAPI=8
   5
   6 inherit check-reqs desktop dune edo
   7
   8 DESCRIPTION="Proof assistant written in O'Caml"
   9 HOMEPAGE="https://coq.inria.fr/
  10         https://github.com/coq/coq/"
  11
  12 if [[ "${PV}" == *9999* ]] ; then
  13         inherit git-r3
  14
  15         EGIT_REPO_URI="https://github.com/coq/coq.git"
  16 else
  17         SRC_URI="https://github.com/coq/coq/archive/V${PV}.tar.gz
  18                 -> ${P}.tar.gz"
  19
  20         KEYWORDS="amd64 ~x86"
  21 fi
  22
  23 LICENSE="LGPL-2.1"
  24 SLOT="0/${PV}"
  25 IUSE="debug doc gui +ocamlopt test"
  26
  27 # TODO: Lots of failing tests. Maybe investigate later.
  28 # RESTRICT="!test? ( test )"
  29 RESTRICT="test"
  30
  31 RDEPEND="
  32         dev-ml/num:=
  33         dev-ml/zarith:=
  34         gui? (
  35                 >=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?]
  36                 >=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?]
  37         )
  38 "
  39 DEPEND="
  40         ${RDEPEND}
  41 "
  42 BDEPEND="
  43         dev-ml/findlib
  44         doc? (
  45                 >=dev-java/antlr-4.7:4
  46                 dev-python/antlr4-python3-runtime
  47                 dev-python/beautifulsoup4
  48                 dev-python/pexpect
  49                 dev-python/sphinx-rtd-theme
  50                 dev-python/sphinxcontrib-bibtex
  51                 dev-tex/latexmk
  52                 dev-texlive/texlive-fontsextra
  53                 dev-texlive/texlive-latexextra
  54                 dev-texlive/texlive-xetex
  55                 media-fonts/freefont
  56         )
  57         test? (
  58                 dev-ml/ounit2
  59         )
  60 "
  61
  62 CHECKREQS_DISK_BUILD="2G"
  63
  64 DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md )
  65 DUNE_PACKAGES=()
  66
  67 src_prepare() {
  68         # Remove bad tests (recursive).
  69         local -a bad_tests=(
  70                 coq-makefile/timing-aggregate
  71                 coq-makefile/timing-error
  72                 coq-makefile/timing-per-file
  73                 coq-makefile/timing-per-line
  74                 coq-makefile/timing-template
  75         )
  76         local bad_test=""
  77         for bad_test in "${bad_tests[@]}" ; do
  78                 if [[ -e "test-suite/${bad_test}" ]] ; then
  79                         rm -r "test-suite/${bad_test}" || die "failed to remove test ${bad_test}"
  80                 else
  81                         ewarn "Test file ${bad_test} does not exist"
  82                 fi
  83         done
  84
  85         default
  86 }
  87
  88 src_configure() {
  89         export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/"
  90
  91         DUNE_PACKAGES=(
  92                 coq-core
  93                 coq-stdlib
  94                 coqide-server
  95                 coq
  96         )
  97         use gui && DUNE_PACKAGES+=( coqide )
  98
  99         emake clean
 100
 101         local -a myconf=(
 102                 -prefix /usr
 103                 -libdir "/usr/$(get_libdir)/coq"
 104                 -mandir /usr/share/man
 105                 -docdir "/usr/share/doc/${PF}"
 106                 -datadir /usr/share/coq
 107                 -configdir "/etc/xdg/${PN}"
 108                 -native-compiler "$(usex ocamlopt yes no)"
 109         )
 110         use debug && myconf+=( -debug )
 111         edo sh ./configure "${myconf[@]}"
 112 }
 113
 114 src_compile() {
 115         emake DUNEOPT="--display=short --profile release" VERBOSE="1" dunestrap
 116
 117         dune-compile "${DUNE_PACKAGES[@]}"
 118
 119         use doc && emake refman-html
 120 }
 121
 122 src_install() {
 123         dune-install "${DUNE_PACKAGES[@]}"
 124
 125         if use gui ; then
 126                 make_desktop_entry coqide "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png"
 127         fi
 128
 129         local ocamlc_where="$(ocamlc -where)"
 130
 131         # Dune installs into /usr/<libdir>/ocaml/<coq> but
 132         # Coq wants /usr/<libdir>/<coq> ; symlink those directories
 133         local sym=""
 134         for sym in "${DUNE_PACKAGES[@]}" ; do
 135                 dosym "${ocamlc_where}/${sym}" "/usr/$(get_libdir)/${sym}"
 136         done
 137
 138         einstalldocs
 139 }