sci-mathematics/isabelle/isabelle-2013.2-r1.ebuild

   1 # Copyright 1999-2015 Gentoo Foundation
   2 # Distributed under the terms of the GNU General Public License v2
   3 # $Id$
   4
   5 EAPI="5"
   6
   7 inherit eutils java-pkg-2 multilib versionator
   8
   9 MY_PN="Isabelle"
  10 MY_PV=$(replace_all_version_separators '-')
  11 MY_P="${MY_PN}${MY_PV}"
  12
  13 JEDIT_PV="20131106"
  14 JEDIT_PN="jedit_build"
  15 JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
  16 JEDIT_IC_PN="${JEDIT_PN}-isabelle-component"
  17 JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}"
  18
  19 JFREECHART_PV="1.0.14-1"
  20 JFREECHART_PN="jfreechart"
  21 JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}"
  22 JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component"
  23 JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}"
  24
  25 POLYML_PV="5.5.1-1"
  26 POLYML_PN="polyml"
  27 POLYML_P="${POLYML_PN}-${POLYML_PV}"
  28 POLYML_IC_PN="${POLYML_PN}-isabelle-component"
  29 POLYML_IC_P="${POLYML_IC_PN}-${POLYML_PV}"
  30
  31 SS="2.11"
  32
  33 DESCRIPTION="Isabelle is a generic proof assistant"
  34 HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html"
  35 SRC_URI="http://www.cl.cam.ac.uk/users/lcp/archive/${MY_P}.tar.gz
  36                 http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz
  37                 http://isabelle.in.tum.de/dist/contrib/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz
  38                 https://dev.gentoo.org/~gienah/snapshots/${POLYML_IC_P}.tar.gz"
  39
  40 LICENSE="BSD"
  41 SLOT="0/${PV}"
  42 KEYWORDS="~amd64 ~x86"
  43 IUSE="doc graphbrowsing ledit readline proofgeneral"
  44
  45 #upstream says
  46 #bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
  47 #for document preparation: complete LaTeX
  48 DEPEND=">=app-shells/bash-3.0:*
  49         dev-java/ant-core:0
  50         >=dev-java/jcommon-1.0.18:1.0
  51         >=dev-java/jfreechart-1.0.14:1.0
  52         >=dev-java/itext-2.1.5:0
  53         dev-java/xml-xmlbeans:1
  54         dev-java/xz-java:0
  55         >=dev-lang/ghc-7.6.3
  56         >=dev-lang/polyml-5.5.1:=[-portable]
  57         >=dev-lang/perl-5.8.8-r2
  58         dev-lang/swi-prolog
  59         virtual/jdk:1.7
  60         doc? (
  61                 virtual/latex-base
  62                 dev-tex/rail
  63         )
  64         >=dev-lang/scala-2.11.1:${SS}
  65         ledit? (
  66                 app-misc/ledit
  67         )
  68         readline? (
  69                 app-misc/rlwrap
  70         )"
  71
  72 RDEPEND="dev-perl/libwww-perl
  73         sci-mathematics/sha1-polyml
  74         >=virtual/jre-1.7
  75         proofgeneral? (
  76                 >=app-emacs/proofgeneral-4.1
  77         )
  78         ${DEPEND}"
  79
  80 S="${WORKDIR}"/Isabelle${MY_PV}
  81 JEDIT_S="${WORKDIR}/${JEDIT_P}"
  82 JFREECHART_S="${WORKDIR}/${JFREECHART_P}"
  83 TARGETDIR="/usr/share/Isabelle"${MY_PV}
  84 LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
  85
  86 # Notes on QA warnings: * Class files not found via DEPEND in package.env
  87 # Stuff with $ in the name appear to be spurious:
  88 # isabelle/Markup_Tree$$anonfun$results$1$1.class
  89 # scala/tools/nsc/backend/jvm/GenJVM$BytecodeGenerator$$anonfun$computeLocalVarsIndex$1.class
  90 # It wants javafx, I am unsure how to fix this. I test isabelle with the Sun JDK:
  91 # javafx/application/Platform.class               javafx
  92 # Presumably the user can provide the jEdit plugins if they are necessary:
  93 # marker/MarkerSetsPlugin.class                   http://plugins.jedit.org/plugins/?MarkerSets
  94 # projectviewer/gui/OptionPaneBase.class          http://plugins.jedit.org/plugins/?ProjectViewer
  95
  96 LIBRARY_PKGS="ant-core,itext,jcommon-1.0,jfreechart-1.0,scala-${SS},xml-xmlbeans-1,xz-java"
  97
  98 src_unpack() {
  99         unpack "${MY_P}.tar.gz"
 100         pushd "${S}/contrib" || die
 101         unpack ${JEDIT_IC_P}.tar.gz
 102         unpack ${JFREECHART_IC_P}.tar.gz
 103         unpack ${POLYML_IC_P}.tar.gz
 104 }
 105
 106 pkg_setup() {
 107         java-pkg-2_pkg_setup
 108 }
 109
 110 src_prepare() {
 111         java-pkg-2_src_prepare
 112         java-pkg_getjars ${LIBRARY_PKGS}
 113         epatch "${FILESDIR}/${PN}-2013-gentoo-settings.patch"
 114         epatch "${FILESDIR}/${PN}-2013.2-classpath.patch"
 115         polymlver=$(poly -v | cut -d' ' -f2)
 116         polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
 117         sed -e "s@5.5.0@${polymlver}@g" \
 118                 -i "${S}/etc/settings" \
 119                 || die "Could not configure polyml version in etc/settings"
 120         sed -e "s@ML_HOME=\"/@ML_HOME=\"${ROOT}@" \
 121                 -i "${S}/etc/settings" \
 122                 || die "Could not configure polyml ML_HOME in etc/settings"
 123         sed -e "s@x86_64@${polymlarch}@g" \
 124                 -i "${S}/etc/settings" \
 125                 || die "Could not configure polyml arch in etc/settings"
 126         sed -e "s@PROOFGENERAL_HOME=\"/@PROOFGENERAL_HOME=\"${ROOT}@" \
 127                 -i "${S}/etc/settings" \
 128                 || die "Could not configure PROOFGENERAL_HOME in etc/settings"
 129         sed -e "s@/usr/lib64/Isabelle${MY_PV}@${LIBDIR}@g" \
 130                 -i "${S}/etc/settings" \
 131                 || die "Could not configure Isabelle lib directory in etc/settings"
 132         epatch "${FILESDIR}/${PN}-2012-graphbrowser.patch"
 133         epatch "${FILESDIR}/${PN}-2012-libsha1.patch"
 134         # this example fails to compile with swi-prolog 6.5.2, so patch it so that
 135         # Isabelle will build, then reverse the patch so that the user can see the
 136         # original code.
 137         epatch "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch"
 138         cat <<- EOF >> "${S}/etc/settings"
 139
 140                 ISABELLE_GHC="${ROOT}usr/bin/ghc"
 141                 ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
 142                 ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
 143                 ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
 144                 SCALA_HOME="${ROOT}usr/share/scala-${SS}"
 145                 SHA1_HOME="/usr/$(get_libdir)/sha1-polyml"
 146         EOF
 147         cat <<- EOF >> "${S}/etc/components"
 148                 #bundled components
 149                 contrib/${JEDIT_P}
 150                 contrib/${JFREECHART_P}
 151                 contrib/${POLYML_P}
 152         EOF
 153         if use ledit && ! use readline; then
 154                 epatch "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
 155         fi
 156         rm -f "${S}/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar" \
 157                 "${S}/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar" \
 158                 "${S}/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar" \
 159                 "${S}/lib/classes/ext/scala-actors.jar" \
 160                 "${S}/lib/classes/ext/scala-compiler.jar" \
 161                 "${S}/lib/classes/ext/scala-library.jar" \
 162                 "${S}/lib/classes/ext/scala-reflect.jar" \
 163                 "${S}/lib/classes/ext/scala-swing.jar" \
 164                 || die "Could not rm bundled jar files supplied by Gentoo"
 165 }
 166
 167 src_compile() {
 168         einfo "Building Isabelle. This may take some time."
 169         ./bin/isabelle build -a -b -s -v || die "isabelle build failed"
 170         epatch --reverse "${FILESDIR}/${PN}-2013.2-HOL-Predicate_Compile_Examples.patch"
 171         if use graphbrowsing
 172         then
 173                 rm -f "${S}/lib/browser/GraphBrowser.jar" \
 174                         || die "failed cleaning graph browser directory"
 175                 pushd "${S}/lib/browser" \
 176                         || die "Could not change directory to lib/browser"
 177                 ./build || die "failed building the graph browser"
 178                 popd
 179         fi
 180         ./bin/isabelle jedit -b -f || die "pide build failed"
 181 }
 182
 183 src_install() {
 184         insinto ${TARGETDIR}
 185         doins -r src
 186         doins -r lib
 187         doins -r contrib
 188         doins ROOTS
 189
 190         docompress -x /usr/share/doc/${PF}
 191         dodoc -r doc
 192         if use doc; then
 193                 dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
 194                 # The build of sci-mathematics/haskabelle with use doc requires
 195                 # sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
 196                 # the src/Doc directory stuff in the isabelle package.
 197                 doins -r src/Doc
 198                 for i in "./src/Doc/Classes/document/build" \
 199                         "./src/Doc/Codegen/document/build" \
 200                         "./src/Doc/Datatypes/document/build" \
 201                         "./src/Doc/fixbookmarks" \
 202                         "./src/Doc/Functions/document/build" \
 203                         "./src/Doc/Intro/document/build" \
 204                         "./src/Doc/IsarImplementation/document/build" \
 205                         "./src/Doc/IsarRef/document/build" \
 206                         "./src/Doc/IsarRef/document/showsymbols" \
 207                         "./src/Doc/JEdit/document/build" \
 208                         "./src/Doc/LaTeXsugar/document/build" \
 209                         "./src/Doc/Locales/document/build" \
 210                         "./src/Doc/Logics/document/build" \
 211                         "./src/Doc/Main/document/build" \
 212                         "./src/Doc/Nitpick/document/build" \
 213                         "./src/Doc/prepare_document" \
 214                         "./src/Doc/ProgProve/document/build" \
 215                         "./src/Doc/sedindex" \
 216                         "./src/Doc/Sledgehammer/document/build" \
 217                         "./src/Doc/System/document/build" \
 218                         "./src/Doc/Tutorial/document/build" \
 219                         "./src/Doc/Tutorial/document/isa-index" \
 220                         "./src/Doc/ZF/document/build"
 221                 do
 222                         exeinto $(dirname "${TARGETDIR}/${i}")
 223                         doexe ${i}
 224                 done
 225         fi
 226
 227         for i in "./bin/isabelle" \
 228                 "./bin/isabelle-process" \
 229                 "./bin/isabelle_scala_script" \
 230                 "./lib/browser/build" \
 231                 "./lib/scripts/feeder" \
 232                 "./lib/scripts/getsettings" \
 233                 "./lib/scripts/polyml-version" \
 234                 "./lib/scripts/process" \
 235                 "./lib/scripts/run-polyml" \
 236                 "./lib/scripts/run-polyml-5.5.1" \
 237                 "./lib/scripts/run-smlnj" \
 238                 "./lib/scripts/unsymbolize" \
 239                 "./lib/scripts/update_sub_sup" \
 240                 "./lib/scripts/yxml" \
 241                 "./lib/Tools/browser" \
 242                 "./lib/Tools/build" \
 243                 "./lib/Tools/components" \
 244                 "./lib/Tools/display" \
 245                 "./lib/Tools/doc" \
 246                 "./lib/Tools/document" \
 247                 "./lib/Tools/emacs" \
 248                 "./lib/Tools/env" \
 249                 "./lib/Tools/findlogics" \
 250                 "./lib/Tools/getenv" \
 251                 "./lib/Tools/install" \
 252                 "./lib/Tools/java" \
 253                 "./lib/Tools/keywords" \
 254                 "./lib/Tools/latex" \
 255                 "./lib/Tools/logo" \
 256                 "./lib/Tools/mkroot" \
 257                 "./lib/Tools/options" \
 258                 "./lib/Tools/scala" \
 259                 "./lib/Tools/scalac" \
 260                 "./lib/Tools/tty" \
 261                 "./lib/Tools/unsymbolize" \
 262                 "./lib/Tools/update_sub_sup" \
 263                 "./lib/Tools/version" \
 264                 "./lib/Tools/yxml" \
 265                 "./src/HOL/IMP/export.sh" \
 266                 "./src/HOL/Library/Sum_of_Squares/neos_csdp_client" \
 267                 "./src/HOL/Mirabelle/lib/Tools/mirabelle" \
 268                 "./src/HOL/Mutabelle/lib/Tools/mutabelle" \
 269                 "./src/HOL/SPARK/Examples/README" \
 270                 "./src/HOL/Tools/ATP/scripts/dummy_atp" \
 271                 "./src/HOL/Tools/ATP/scripts/remote_atp" \
 272                 "./src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py" \
 273                 "./src/HOL/Tools/Sledgehammer/MaSh/src/mash.py" \
 274                 "./src/HOL/Tools/Sledgehammer/MaSh/src/server.py" \
 275                 "./src/HOL/Tools/SMT/lib/scripts/remote_smt" \
 276                 "./src/HOL/TPTP/lib/Tools/tptp_graph" \
 277                 "./src/HOL/TPTP/lib/Tools/tptp_isabelle" \
 278                 "./src/HOL/TPTP/lib/Tools/tptp_isabelle_hot" \
 279                 "./src/HOL/TPTP/lib/Tools/tptp_nitpick" \
 280                 "./src/HOL/TPTP/lib/Tools/tptp_refute" \
 281                 "./src/HOL/TPTP/lib/Tools/tptp_sledgehammer" \
 282                 "./src/HOL/TPTP/TPTP_Parser/make_mlyacclib" \
 283                 "./src/HOL/TPTP/TPTP_Parser/make_tptp_parser" \
 284                 "./src/Pure/build" \
 285                 "./src/Pure/build-jars" \
 286                 "./src/Tools/Code/lib/Tools/codegen" \
 287                 "./src/Tools/Graphview/lib/Tools/graphview" \
 288                 "./src/Tools/jEdit/lib/Tools/jedit" \
 289                 "./src/Tools/Metis/fix_metis_license" \
 290                 "./src/Tools/Metis/make_metis" \
 291                 "./src/Tools/Metis/scripts/mlpp" \
 292                 "./src/Tools/WWW_Find/lib/Tools/wwwfind"
 293         do
 294                 exeinto $(dirname "${TARGETDIR}/${i}")
 295                 doexe ${i}
 296         done
 297
 298         insinto /etc/isabelle
 299         doins -r etc/*
 300         dosym /etc/isabelle "${TARGETDIR}/etc"
 301
 302         dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
 303         insinto ${LIBDIR}
 304         doins -r heaps
 305
 306         bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \
 307                 || die "isabelle install failed"
 308         newicon lib/icons/"${PN}.xpm" "${PN}.xpm"
 309         newicon lib/icons/"${PN}-mini.xpm" "${PN}-mini.xpm"
 310         dodoc ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README
 311
 312         java-pkg_regjar \
 313                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Console.jar" \
 314                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/ErrorList.jar" \
 315                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/Highlight.jar" \
 316                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/idea-icons.jar" \
 317                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jars/QuickNotepad.jar" \
 318                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jedit-5.1.0-patched/jedit.jar" \
 319                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/jsr305-2.0.0.jar" \
 320                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/MacOSX.jar" \
 321                 "${ED}${TARGETDIR}/contrib/${JEDIT_P}/contrib/SideKick.jar" \
 322                 "${ED}${TARGETDIR}/contrib/${JFREECHART_P}/jfreechart-1.0.14-demo.jar" \
 323                 "${ED}${TARGETDIR}/lib/browser/GraphBrowser.jar" \
 324                 "${ED}${TARGETDIR}/lib/classes/Graphview.jar" \
 325                 "${ED}${TARGETDIR}/lib/classes/Pure.jar" \
 326                 "${ED}${TARGETDIR}/lib/classes/scala-actors.jar" \
 327                 "${ED}${TARGETDIR}/lib/classes/scala-compiler.jar" \
 328                 "${ED}${TARGETDIR}/lib/classes/scala-library.jar" \
 329                 "${ED}${TARGETDIR}/lib/classes/scala-reflect.jar" \
 330                 "${ED}${TARGETDIR}/lib/classes/scala-swing.jar" \
 331                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Console.jar" \
 332                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/ErrorList.jar" \
 333                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Highlight.jar" \
 334                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/idea-icons.jar" \
 335                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar" \
 336                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/jsr305-2.0.0.jar" \
 337                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/MacOSX.jar" \
 338                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/QuickNotepad.jar" \
 339                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jars/SideKick.jar" \
 340                 "${ED}${TARGETDIR}/src/Tools/jEdit/dist/jedit.jar"
 341 }
 342
 343 pkg_postinst() {
 344         # If any of the directories in /etc/isabelle/components do not exist, then
 345         # even isabelle getenv ISABELLE_HOME fails.  Hence it is necessary to
 346         # to delete any non-existing directories.  If an old Isabelle version was
 347         # installed with component ebuilds like sci-mathematics/e, then the
 348         # Isabelle version is upgraded, then the contrib directories will not
 349         # exist initially, it is necessary to delete them from /etc/isabelle/components.
 350         # Then these components are rebuilt (creating these directories) using the
 351         # EAPI=5 subslot depends.
 352         for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
 353         do
 354                 if [ ! -d /usr/share/${MY_P}/${i} ]; then
 355                         sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
 356                 fi
 357         done
 358         if use ledit && use readline; then
 359                 elog "Both readline and ledit use flags specified.  The default setting"
 360                 elog "if both are installed is to use readline (rlwrap), this can be"
 361                 elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
 362                 elog "${ROOT}/etc/isabelle/settings"
 363         fi
 364         elog "Please ensure you have a pdf viewer installed, for example:"
 365         elog "As root: emerge app-text/zathura-pdf-poppler"
 366         elog "Please configure your preferred pdf viewer, something like:"
 367         elog "As normal user: xdg-mime default zathura.desktop application/pdf"
 368         elog "Or alternatively by editing the PDF_VIEWER variable in the system"
 369         elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
 370         elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
 371         elog "To improve sledgehammer performance, consider installing:"
 372         elog "USE=isabelle emerge sci-mathematics/e sci-mathematics/spass"
 373         elog "For nitpick it is necessary to install:"
 374         elog "emerge sci-mathematics/kodkodi"
 375 }