gentoo-mirror/gentoo
1
0
Fork 0
mirror of https://github.com/gentoo-mirror/gentoo.git synced 2026-11-09 18:47:16 -08:00
Code Issues Projects Releases Wiki Activity

sci-mathematics/isabelle: Remove last-rited pkg

Browse Source 
Signed-off-by: Michał Górny <mgorny@gentoo.org>
This commit is contained in:
Michał Górny
2019-09-14 17:44:37 +02:00
parent 1c1e7716d8
commit 7d2aafd09b
14 changed files with 0 additions and 648 deletions
Download Patch File Download Diff File Expand all files Collapse all files
profiles/package.mask
-1
View File
@@ -1116,7 +1116,6 @@ dev-java/itext
app-text/jpdftweak
dev-util/deskzilla
media-sound/tuxguitar
sci-mathematics/isabelle
# Michał Górny <mgorny@gentoo.org> (2019-08-14)
# No longer builds. Homepage is gone, and its keep-alive fork is also
sci-mathematics/isabelle/Manifest
-10
View File
@@ -1,10 +0,0 @@
DIST Isabelle2016-1.tar.gz 39567637 BLAKE2B a664c89f2705e6b2709a8b3054d57ca443435967dd85f07e1651aa0bbfc41ee31dee88146243c8e0bddc2a1de86107158a89d13b2ff427f8dcf0308fe3dd2654 SHA512 c7da7900033a8c816f002b8899e398da7819dc457b3b1176dc9a19adffeb42d5524f2d14581a391487da1f36ffeabd0867bacab6462f3decfc0f7a9caf81a2d2
DIST bash_process-isabelle-component-1.2.1.tar.gz 33182 BLAKE2B d139f5476b02b22a896fa742303a4e5c4de583972eb38a67e1a451fabe28d52c2c1310be865faf244104cad46758e1bf97f6222170999ff2e2da7c07e1398fe3 SHA512 d9817191af5660e38f1647401803115a93f0052291bfbbcb1cd9b41a4bab89b3ebdde22b40744a04ad3268aed8ca037ae59981c513f71b3ff6d89855d29e14c3
DIST csdp-isabelle-component-6.x.tar.gz 493 BLAKE2B 364c8f390adfb4031958597e4435783e58ebbb3be49ee80d5ee6631770d9322190bd364530622ae66d490d91e499bb3bb626b01762fccf3f67c65b20b3f7756b SHA512 9be28ecbf61d0f6ad23e28d44bd7ceb8f06ab22f3a05a7c823a9c5bf52ddcf5e5c300c41e14451d6b8e6a4c32b1bbd17769c731cd890fab335a866cd5e735290
DIST isabelle_fonts-isabelle-component-20160830.tar.gz 249427 BLAKE2B 8398e578e6b8f54ac163b33e29c8283fef29c5db2cd8562dca1d636e1947bebb54e79e55035398fca215f2fbdf868dfe318d91a7f76074ad97f2d4792b8b4432 SHA512 a185f79990478861832e9400ea37ffd02f582d3f916d26d901b8b0ec923027c412538bafe4a763a132adb9277a4b00a7a510762928ec49433ef550ae3fe59dbc
DIST jedit_build-isabelle-component-20161024.tar.gz 10819946 BLAKE2B 2764d854eecd6783a0893934742f21db9ac47b1304f969803e01ffc402d57d2f3d38c9f07cb6ea6d77f12a48337892baecc7175b1d759989d7c46d0104b34a9f SHA512 0563b696307dd33b244e4ecc62664056a2b003c3291a5e3d7dd4f1c936dac2c3257ff90273cb2c8dc3bf9dea40fae745fabb57fc5f4ed420d0c8fd7d2b917433
DIST jfreechart-isabelle-component-1.0.14-1.tar.gz 3444825 BLAKE2B 4a24f362d647c9bbe538d18a49f7579cf9c1914854b19c7f4cca29d876870eb5f994df4b53ae2bf6f8bf8aa697306bfebdb272493fb974c6df8050778d173376 SHA512 ee1d84a45e43029d5e3acee823176196da19789322e8d3c2c81d5504930ad81d50e16e5da87655e4151034901daefb4ce6b82334839e39134b3a7ce32203aa67
DIST jortho-isabelle-component-1.0-2.tar.gz 1723761 BLAKE2B 4f5503c640d25d79a8520a2f137900a8397db141f5f6279e4622bf44c377a3bcd7224d9e59de2f57993867362350bc279aebc54dc548562bab6b78b210110fb7 SHA512 8bef5e025d13b76c86a727bf93887b846cc906b2ce00299c38f69ccf33fb9dc7411e55b6fd1c56ed993c180d83a7e9ed90122f7feb6ae4fb70df93802ac21211
DIST polyml-isabelle-component-5.6-1.tar.gz 822 BLAKE2B eea808d3cd2ce2c6b5b531fce046eba59e39f671e48e76e3d9093a4d9fadef9fbf3afc20b98eeaf5e672e8e34ed11aaf62441266469f53d3d228252fe9f64f89 SHA512 403239aa48aab8c39e12cd5f82cb5e3ba7c31f9325d88f5137d3ec509bb25ab4eb8b1103a66b8ea5ad45c7c968ef092749c486217528a5db4223819106c00a59
DIST ssh-java-isabelle-component-20161009.tar.gz 412919 BLAKE2B d05152d92669043ba23d7e0767470a529ac7688866ed8be64432d724329a0c24590586faf5e09c365c44740550441798681b9e8b80a323285516ec61a884beb8 SHA512 685a9b8791046c1bc21aa77614fb1b304e7438715377e179954ebfd1603434ff66fe23e90de928a5af6f51a48ae6ea6f05f9ff8941d98f7c3a43fdda02d3b519
DIST xz-java-isabelle-component-1.5.tar.gz 315 BLAKE2B b7a385671469fb8643d74d90b4faae2f66621f7bafb0262b7fc7777c883cae4a5939cb5261230c21a6125ce12cafe5285a873fc0a37f78ef0e4059d310c2bd0e SHA512 6dfec49e12c4cafbb6b6386dd54477e86b6bb419a77c52d9606a0305aeea9cd11f087ed6bba77352c7bf9ec656052ef617e845f472e57b5cdfbccf22b2eeb4fa
sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch
-11
View File
@@ -1,11 +0,0 @@
--- Isabelle2012-orig/lib/browser/build 2012-05-20 19:34:33.000000000 +1000
+++ Isabelle2012/lib/browser/build 2012-05-26 22:18:41.952750622 +1000
@@ -6,6 +6,8 @@
#
# Requires proper Isabelle settings environment.
+ISABELLE_HOME="$(cd "$(dirname "${0}")/../.."; pwd -P)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
## diagnostics
sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch
-12
View File
@@ -1,12 +0,0 @@
--- Isabelle2012-orig/etc/settings 2012-05-23 03:07:38.000000000 +1000
+++ Isabelle2012/etc/settings 2012-05-27 12:43:36.209715015 +1000
@@ -62,8 +62,8 @@
###
ISABELLE_LINE_EDITOR=""
-[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
###
sci-mathematics/isabelle/files/isabelle-2016-classpath.patch
-32
View File
@@ -1,32 +0,0 @@
Index: Isabelle2016/lib/Tools/java
===================================================================
--- Isabelle2016.orig/lib/Tools/java
+++ Isabelle2016/lib/Tools/java
@@ -10,5 +10,5 @@ declare -a JAVA_ARGS; eval "JAVA_ARGS=($
unset CLASSPATH
isabelle_java java "${JAVA_ARGS[@]}" \
- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
Index: Isabelle2016/lib/Tools/scala
===================================================================
--- Isabelle2016.orig/lib/Tools/scala
+++ Isabelle2016/lib/Tools/scala
@@ -14,4 +14,4 @@ do
done
isabelle_scala scala "${SCALA_ARGS[@]}" \
- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
Index: Isabelle2016/lib/Tools/scalac
===================================================================
--- Isabelle2016.orig/lib/Tools/scalac
+++ Isabelle2016/lib/Tools/scalac
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH:$(java-config -p scala-2.11)")" "$@"
sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch
-16
View File
@@ -1,16 +0,0 @@
--- Isabelle2016-orig/contrib/jfreechart-1.0.14-1/etc/settings 2013-09-12 07:46:57.000000000 +1000
+++ Isabelle2016/contrib/jfreechart-1.0.14-1/etc/settings 2016-07-07 17:22:55.716464804 +1000
@@ -1,9 +1,8 @@
# -*- shell-script -*- :mode=shellscript:
JFREECHART_HOME="$COMPONENT"
-JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar"
-
-classpath "$JFREECHART_HOME/lib/iText-2.1.5.jar"
-classpath "$JFREECHART_HOME/lib/jcommon-1.0.18.jar"
-classpath "$JFREECHART_HOME/lib/jfreechart-1.0.14.jar"
+JFREECHART_JAR_NAMES="$(java-config --classpath itext | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jcommon-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g') $(java-config --classpath jfreechart-1.0 | sed -e 's@:@ @g' -e 's@/[^ ]*/@@g')"
+classpath "$(java-config --classpath itext)"
+classpath "$(java-config --classpath jcommon-1.0)"
+classpath "$(java-config --classpath jfreechart-1.0)"
sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch
-7
View File
@@ -1,7 +0,0 @@
--- Isabelle2016-1-orig/contrib/bash_process-1.2.1/etc/settings 2016-02-14 09:48:03.000000000 +1100
+++ Isabelle2016-1/contrib/bash_process-1.2.1/etc/settings 2017-01-02 13:44:49.355549312 +1100
@@ -1,3 +1,3 @@
# -*- shell-script -*- :mode=shellscript:
-ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
+ISABELLE_BASH_PROCESS="$COMPONENT/bash_process"
sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch
-128
View File
@@ -1,128 +0,0 @@
--- Isabelle2016-1-orig/src/Tools/jEdit/lib/Tools/jedit 2016-12-13 01:03:49.000000000 +1100
+++ Isabelle2016-1/src/Tools/jEdit/lib/Tools/jedit 2017-01-01 17:24:50.107722845 +1100
@@ -239,125 +239,6 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
)
-
-# target
-
-TARGET="dist/jars/Isabelle-jEdit.jar"
-
-declare -a UPDATED=()
-
-if [ "$BUILD_JARS" = jars_fresh ]; then
- OUTDATED=true
-else
- OUTDATED=false
- if [ ! -e "$TARGET" ]; then
- OUTDATED=true
- else
- if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- declare -a DEPS=(
- "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
- "${SOURCES[@]}" "${RESOURCES[@]}"
- )
- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
- else
- declare -a DEPS=()
- fi
- for DEP in "${DEPS[@]}"
- do
- [ ! -e "$DEP" ] && fail "Missing file: $DEP"
- [ "$DEP" -nt "$TARGET" ] && {
- OUTDATED=true
- UPDATED["${#UPDATED[@]}"]="$DEP"
- }
- done
- fi
-fi
-
-
-# build
-
-if [ "$OUTDATED" = true ]
-then
- echo "### Building Isabelle/jEdit ..."
-
- [ "${#UPDATED[@]}" -gt 0 ] && {
- echo "Changed files:"
- for FILE in "${UPDATED[@]}"
- do
- echo " $FILE"
- done
- }
-
- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
- rm -rf dist || failed
- mkdir -p dist dist/classes || failed
-
- cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
- cp -p -R -f "${RESOURCES[@]}" dist/classes/.
- cp src/jEdit.props dist/properties/.
- cp -p -R -f src/modes/. dist/modes/.
-
- perl -i -e 'while (<>) {
- if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
- elsif (m/NAME="javacc"/) {
- print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
- print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
- print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
- print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
- print qq!<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n!;
- print;
- }
- elsif (m/NAME="sqr"/) {
- print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
- print;
- }
- else { print; }
- }' dist/modes/catalog
-
- cd dist
- isabelle_jdk jar xf jedit.jar
- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
- "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
- "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
- isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
- rm -rf META-INF org
- cd ..
-
- cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
- (
- #FIXME workarounds for scalac 2.11.0
- export CYGWIN="nodosfilewarning"
- function stty() { :; }
- export -f stty
-
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
- do
- classpath "$JAR"
- done
- export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
- exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
- ) || fail "Failed to compile sources"
-
- cd dist/classes
- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
- cd ../..
- rm -rf dist/classes
-
- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf
- cp dist/doc/CHANGES.txt dist/doc/jedit-changes
- cat > dist/doc/Contents <<EOF
-Original jEdit Documentation
- jedit-manual jEdit 5.3 User's Guide
- jedit-changes jEdit 5.3 Version History
-
-EOF
-
-fi
-
popd >/dev/null
sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch
-8
View File
@@ -1,8 +0,0 @@
--- Isabelle2016-1-orig/contrib/jortho-1.0-2/etc/settings 2014-04-16 06:03:34.000000000 +1000
+++ Isabelle2016-1/contrib/jortho-1.0-2/etc/settings 2017-01-02 00:13:01.619790577 +1100
@@ -3,4 +3,4 @@
JORTHO_HOME="$COMPONENT"
JORTHO_DICTIONARIES="$JORTHO_HOME/dictionaries/en.gz:$JORTHO_HOME/dictionaries/en_US.gz:$JORTHO_HOME/dictionaries/en_GB-ise.gz:$JORTHO_HOME/dictionaries/en_GB-ize.gz:$JORTHO_HOME/dictionaries/en_CA.gz"
-classpath "$JORTHO_HOME/jortho.jar"
+classpath "$(java-config -p jortho)"
sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch
-11
View File
@@ -1,11 +0,0 @@
--- Isabelle2016-1-orig/src/Pure/General/sha1.ML 2016-12-13 01:03:45.000000000 +1100
+++ Isabelle2016-1/src/Pure/General/sha1.ML 2016-12-28 20:50:36.814706587 +1100
@@ -146,7 +146,7 @@
(* C library and memory *)
val library_path =
- Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
+ Path.explode ("$SHA1_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
fun with_memory n =
Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch
-33
View File
@@ -1,33 +0,0 @@
--- Isabelle2016-1-orig/src/HOL/SMT_Examples/Boogie.thy 2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/Boogie.thy 2016-12-30 23:46:11.947737290 +1100
@@ -52,7 +52,7 @@
section \<open>Verification condition proofs\<close>
declare [[smt_oracle = false]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
declare [[smt_certificates = "Boogie_Max.certs"]]
--- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-30 23:46:11.953737338 +1100
@@ -9,7 +9,7 @@
begin
declare [[smt_certificates = "SMT_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
section \<open>Propositional and first-order logic\<close>
--- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-30 23:46:11.967737450 +1100
@@ -11,7 +11,7 @@
declare [[smt_oracle = true]]
declare [[z3_extensions = true]]
declare [[smt_certificates = "SMT_Word_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
text \<open>
Currently, there is no proof reconstruction for words.
sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch
-22
View File
@@ -1,22 +0,0 @@
--- Isabelle2016-1-orig/src/HOL/SMT.thy 2016-12-13 01:03:38.000000000 +1100
+++ Isabelle2016-1/src/HOL/SMT.thy 2016-12-30 14:11:09.379863215 +1100
@@ -201,7 +201,7 @@
(given in seconds) to restrict their runtime.
\<close>
-declare [[smt_timeout = 20]]
+declare [[smt_timeout = 300]]
text \<open>
SMT solvers apply randomized heuristics. In case a problem is not
--- Isabelle2016-1-orig/src/HOL/Tools/SMT/smt_config.ML 2016-12-13 01:03:42.000000000 +1100
+++ Isabelle2016-1/src/HOL/Tools/SMT/smt_config.ML 2016-12-30 14:11:27.186904132 +1100
@@ -170,7 +170,7 @@
(* options *)
val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
-val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
+val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 300.0)
val reconstruction_step_timeout = Attrib.setup_config_real @{binding smt_reconstruction_step_timeout} (K 10.0)
val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
val read_only_certificates = Attrib.setup_config_bool @{binding smt_read_only_certificates} (K false)
sci-mathematics/isabelle/isabelle-2016.1.ebuild
-328
View File
@@ -1,328 +0,0 @@
# Copyright 1999-2018 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI="6"
inherit eutils check-reqs java-pkg-2 versionator
MY_PN="Isabelle"
MY_PV=$(replace_all_version_separators '-')
MY_P="${MY_PN}${MY_PV}"
BP_PV="1.2.1"
BP_PN="bash_process"
BP_P="${BP_PN}-${BP_PV}"
BP_IC_PN="${BP_PN}-isabelle-component"
BP_IC_P="${BP_IC_PN}-${BP_PV}"
# csdp is used in the compile of HOL_ex in
# Library/Sum_of_Squares/sos_wrapper.ML where it execs $ISABELLE_CSDP
CSDP_PV="6.x"
CSDP_PN="csdp"
CSDP_P="${CSDP_PN}-${CSDP_PV}"
CSDP_IC_PN="${CSDP_PN}-isabelle-component"
CSDP_IC_P="${CSDP_IC_PN}-${CSDP_PV}"
ISABELLE_FONTS_PV="20160830"
ISABELLE_FONTS_PN="isabelle_fonts"
ISABELLE_FONTS_P="${ISABELLE_FONTS_PN}-${ISABELLE_FONTS_PV}"
ISABELLE_FONTS_IC_PN="${ISABELLE_FONTS_PN}-isabelle-component"
ISABELLE_FONTS_IC_P="${ISABELLE_FONTS_IC_PN}-${ISABELLE_FONTS_PV}"
JEDIT_PV="20161024"
JEDIT_PN="jedit_build"
JEDIT_P="${JEDIT_PN}-${JEDIT_PV}"
JEDIT_IC_PN="${JEDIT_PN}-isabelle-component"
JEDIT_IC_P="${JEDIT_IC_PN}-${JEDIT_PV}"
JORTHO_PV="1.0-2"
JORTHO_PN="jortho"
JORTHO_P="${JORTHO_PN}-${JORTHO_PV}"
JORTHO_IC_PN="${JORTHO_PN}-isabelle-component"
JORTHO_IC_P="${JORTHO_IC_PN}-${JORTHO_PV}"
JFREECHART_PV="1.0.14-1"
JFREECHART_PN="jfreechart"
JFREECHART_P="${JFREECHART_PN}-${JFREECHART_PV}"
JFREECHART_IC_PN="${JFREECHART_PN}-isabelle-component"
JFREECHART_IC_P="${JFREECHART_IC_PN}-${JFREECHART_PV}"
POLYML_PV="5.6-1"
POLYML_PN="polyml"
POLYML_P="${POLYML_PN}-${POLYML_PV}"
POLYML_IC_PN="${POLYML_PN}-isabelle-component"
POLYML_IC_P="${POLYML_IC_PN}-${POLYML_PV}"
SSH_JAVA_PV="20161009"
SSH_JAVA_PN="ssh-java"
SSH_JAVA_P="${SSH_JAVA_PN}-${SSH_JAVA_PV}"
SSH_JAVA_IC_PN="${SSH_JAVA_PN}-isabelle-component"
SSH_JAVA_IC_P="${SSH_JAVA_IC_PN}-${SSH_JAVA_PV}"
XZ_JAVA_PV="1.5"
XZ_JAVA_PN="xz-java"
XZ_JAVA_P="${XZ_JAVA_PN}-${XZ_JAVA_PV}"
XZ_JAVA_IC_PN="${XZ_JAVA_PN}-isabelle-component"
XZ_JAVA_IC_P="${XZ_JAVA_IC_PN}-${XZ_JAVA_PV}"
SS="2.12"
DESCRIPTION="Isabelle is a generic proof assistant"
HOMEPAGE="http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html"
SRC_URI="http://isabelle.in.tum.de/website-${MY_P}/dist/${MY_P}.tar.gz
http://isabelle.in.tum.de/dist/contrib/${BP_P}.tar.gz -> ${BP_IC_P}.tar.gz
https://dev.gentoo.org/~gienah/snapshots/${CSDP_IC_P}.tar.gz
http://isabelle.in.tum.de/dist/contrib/${ISABELLE_FONTS_P}.tar.gz -> ${ISABELLE_FONTS_IC_P}.tar.gz
http://isabelle.in.tum.de/components/${JORTHO_P}.tar.gz -> ${JORTHO_IC_P}.tar.gz
http://isabelle.in.tum.de/components/${JEDIT_P}.tar.gz -> ${JEDIT_IC_P}.tar.gz
http://isabelle.in.tum.de/dist/contrib/${JFREECHART_P}.tar.gz -> ${JFREECHART_IC_P}.tar.gz
https://dev.gentoo.org/~gienah/snapshots/${POLYML_IC_P}.tar.gz
http://isabelle.in.tum.de/dist/contrib/${SSH_JAVA_P}.tar.gz -> ${SSH_JAVA_IC_P}.tar.gz
https://dev.gentoo.org/~gienah/snapshots/${XZ_JAVA_IC_P}.tar.gz"
LICENSE="BSD"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
IUSE="doc graphbrowsing ledit readline"
#upstream says
#bash 2.x/3.x, Poly/ML 5.x, Perl 5.x,
#for document preparation: complete LaTeX
DEPEND=">=app-shells/bash-3.0:*
>=dev-java/jcommon-1.0.18:1.0
dev-java/jortho:0
>=dev-java/jfreechart-1.0.14:1.0
>=dev-java/itext-2.1.5:0
dev-java/xz-java:0
>=dev-lang/ghc-7.6.3
>=dev-lang/polyml-5.6:=[-portable]
>=dev-lang/perl-5.8.8-r2
>=dev-lang/swi-prolog-6.6.6
sci-libs/coinor-csdp
=sci-mathematics/z3-4.4*[isabelle]
>=virtual/jdk-1.8
doc? (
virtual/latex-base
dev-tex/rail
)
dev-lang/scala:${SS}
ledit? (
app-misc/ledit
)
readline? (
app-misc/rlwrap
)"
RDEPEND="
dev-perl/libwww-perl
sci-mathematics/sha1-polyml
>=virtual/jre-1.8"
S="${WORKDIR}"/Isabelle${MY_PV}
TARGETDIR="/usr/share/Isabelle"
# Notes on QA warnings: * Class files not found via DEPEND in package.env
# Stuff with $ in the name appear to be spurious:
# isabelle/Markup_Tree$$anonfun$results$1$1.class
# scala/tools/nsc/backend/jvm/GenJVM$BytecodeGenerator$$anonfun$computeLocalVarsIndex$1.class
# It wants javafx, I am unsure how to fix this. I test isabelle with the Sun JDK:
# javafx/application/Platform.class javafx
# Presumably the user can provide the jEdit plugins if they are necessary:
# marker/MarkerSetsPlugin.class http://plugins.jedit.org/plugins/?MarkerSets
# projectviewer/gui/OptionPaneBase.class http://plugins.jedit.org/plugins/?ProjectViewer
JAVA_GENTOO_CLASSPATH="itext,jcommon-1.0,jortho,jfreechart-1.0,scala-${SS},xz-java"
CHECKREQS_MEMORY="8192M"
CHECKREQS_DISK_BUILD="17G"
CHECKREQS_DISK_USR="8G"
src_unpack() {
unpack "${MY_P}.tar.gz"
cd "${S}/contrib" || die
unpack ${BP_IC_P}.tar.gz
unpack ${CSDP_IC_P}.tar.gz
unpack ${ISABELLE_FONTS_IC_P}.tar.gz
unpack ${JEDIT_IC_P}.tar.gz
unpack ${JORTHO_IC_P}.tar.gz
unpack ${JFREECHART_IC_P}.tar.gz
unpack ${POLYML_IC_P}.tar.gz
unpack ${SSH_JAVA_IC_P}.tar.gz
unpack ${XZ_JAVA_IC_P}.tar.gz
}
pkg_setup() {
java-pkg-2_pkg_setup
check-reqs_pkg_setup
}
src_prepare() {
java-pkg-2_src_prepare
java-pkg_getjars ${JAVA_GENTOO_CLASSPATH}
rm -rf "${S}/contrib/${BP_P}/{x86-cygwin,x86-darwin,x86_64-darwin,x86-linux,x86_64-linux}" \
|| die "Could not remove bash_process binaries"
rm -f "${S}/contrib/${JORTHI_P}/${JORTHO_PN}.jar" \
|| die "Could not remove contrib/${JORTHI_P}/${JORTHO_PN}.jar"
eapply "${FILESDIR}/${PN}-2016-classpath.patch"
eapply "${FILESDIR}/${PN}-2016-jfreechart-classpath.patch"
eapply "${FILESDIR}/${PN}-2016.1-bash_process-1.2.1-settings.patch"
eapply "${FILESDIR}/${PN}-2012-graphbrowser.patch"
eapply "${FILESDIR}/${PN}-2016.1-libsha1.patch"
eapply "${FILESDIR}/${PN}-2016.1-smt_timeout.patch"
eapply "${FILESDIR}/${PN}-2016.1-smt_read_only_certificates.patch"
eapply "${FILESDIR}/${PN}-2016.1-disable-jedit-build-after-install.patch"
eapply "${FILESDIR}/${PN}-2016.1-jortho-1.0-2-classpath.patch"
local polymlver=$(poly -v | cut -d' ' -f2)
local polymlarch=$(poly -v | cut -d' ' -f9 | cut -d'-' -f1)
cat <<- EOF >> "${S}/etc/settings"
# Poly/ML Gentoo (${polymlarch,,})
ML_PLATFORM=${polymlarch,,}-linux
ML_HOME="${ROOT}usr/bin"
ML_SYSTEM=polyml-${polymlver}
ML_OPTIONS="-H 1000"
ML_SOURCES="${ROOT}usr/src/debug/dev-lang/polyml-${polymlver}"
ISABELLE_GHC="${ROOT}usr/bin/ghc"
ISABELLE_OCAML="${ROOT}usr/bin/ocaml"
ISABELLE_SWIPL="${ROOT}usr/bin/swipl"
ISABELLE_JDK_HOME="\$(java-config --jdk-home)"
ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true"
SCALA_HOME="${ROOT}usr/share/scala-${SS}"
SHA1_HOME="${ROOT}usr/$(get_libdir)/sha1-polyml"
EOF
local Z3_P="$(best_version sci-mathematics/z3 | sed 's:sci-mathematics/::')"
cat <<- EOF >> "${S}/etc/components"
#bundled components
contrib/${BP_P}
contrib/${CSDP_P}
contrib/${ISABELLE_FONTS_P}
contrib/${JEDIT_P}
contrib/${JORTHO_P}
contrib/${JFREECHART_P}
contrib/${POLYML_P}
contrib/${SSH_JAVA_P}
contrib/${XZ_JAVA_P}
contrib/${Z3_P}
EOF
local Z3_RC="${ROOT}usr/share/Isabelle/contrib/${Z3_P}"
[ -d "${Z3_RC}" ] \
|| die "z3 isabelle component directory ${Z3_RC} does not exist"
ln -s "${Z3_RC}" \
"${S}/contrib/${Z3_P}" \
|| die "Failed to create z3 isabelle component symbolic link"
if use ledit && ! use readline; then
eapply "${FILESDIR}/${PN}-2012-reverse-line-editor-order.patch"
fi
rm -f "${S}/contrib/${JFREECHART_P}/lib"/*.jar \
|| die "Could not rm bundled jar files supplied by Gentoo"
}
src_compile() {
unset DISPLAY
einfo "Building Isabelle. This may take some time."
pushd contrib/${BP_P} || die "Could not cd to contrib/${BP_P}"
$(tc-getCC) ${CFLAGS} ${LDFLAGS} -o ${BP_PN} ${BP_PN}.c \
|| die "Could not build ${BP_PN}"
popd || die
if use graphbrowsing
then
rm -f "${S}/lib/browser/GraphBrowser.jar" \
|| die "failed cleaning graph browser directory"
pushd "${S}/lib/browser" \
|| die "Could not change directory to lib/browser"
./build || die "failed building the graph browser"
popd
fi
./bin/isabelle jedit -b -f || die "pide build failed"
pushd "${S}"/src/Pure || die "Could not change directory to src/Pure"
../../bin/isabelle env ./build-jars -f || die "build-jars failed"
popd || die
./bin/isabelle build -a -b -s -v || die "isabelle build failed"
}
src_install() {
local Z3_P="$(best_version sci-mathematics/z3 | sed 's:sci-mathematics/::')"
rm "${S}/contrib/${Z3_P}" \
|| die "Failed to remove z3 isabelle component symbolic link"
insinto ${TARGETDIR}
doins -r src
doins -r lib
doins -r contrib
doins ROOTS
docompress -x /usr/share/doc/${PF}
dodoc -r doc
if use doc; then
dosym /usr/share/doc/${PF}/doc "${TARGETDIR}/doc"
# The build of sci-mathematics/haskabelle with use doc requires
# sci-mathematics/isabelle[doc?]. The haskabelle doc build requires
# the src/Doc directory stuff in the isabelle package.
doins -r src/Doc
for i in $(find ./src/Doc -type f -executable -print)
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
fi
for i in $(find \
./{bin,lib,"contrib/${BP_P}/${BP_PN}",src/HOL,src/Pure,src/Tools} \
-type f -executable -print)
do
exeinto $(dirname "${TARGETDIR}/${i}")
doexe ${i}
done
insinto /etc/isabelle
doins -r etc/*
dosym /etc/isabelle "${TARGETDIR}/etc"
local LIBDIR="/usr/"$(get_libdir)"/Isabelle"${MY_PV}
dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps"
insinto ${LIBDIR}
doins -r heaps
./bin/isabelle install -d ${TARGETDIR} "${ED}usr/bin" \
|| die "isabelle install failed"
newicon lib/icons/"${PN}.xpm" "${PN}.xpm"
newicon lib/icons/"${PN}-mini.xpm" "${PN}-mini.xpm"
java-pkg_regjar \
$(find . -type f -name \*.jar -print | sed -e "s@^\.@${ED}${TARGETDIR}@g")
local DOCS=( "ANNOUNCE" "CONTRIBUTORS" "COPYRIGHT" "NEWS" "README" )
einstalldocs
}
pkg_postinst() {
# If any of the directories in /etc/isabelle/components do not exist, then
# even isabelle getenv ISABELLE_HOME fails. Hence it is necessary to
# to delete any non-existing directories. If an old Isabelle version was
# installed with component ebuilds like sci-mathematics/e, then the
# Isabelle version is upgraded, then the contrib directories will not
# exist initially, it is necessary to delete them from /etc/isabelle/components.
# Then these components are rebuilt (creating these directories) using the
# EAPI=5 subslot depends.
for i in $(egrep '^[^#].*$' "${ROOT}etc/isabelle/components")
do
if [ ! -d ${TARGETDIR}/${i} ]; then
sed -e "\@${i}@d" -i "${ROOT}etc/isabelle/components"
fi
done
if use ledit && use readline; then
elog "Both readline and ledit use flags specified. The default setting"
elog "if both are installed is to use readline (rlwrap), this can be"
elog "modfied by editing the ISABELLE_LINE_EDITOR setting in"
elog "${ROOT}/etc/isabelle/settings"
fi
elog "Please ensure you have a pdf viewer installed, for example:"
elog "As root: emerge app-text/zathura-pdf-poppler"
elog "Please configure your preferred pdf viewer, something like:"
elog "As normal user: xdg-mime default zathura.desktop application/pdf"
elog "Or alternatively by editing the PDF_VIEWER variable in the system"
elog "settings file ${ROOT}etc/isabelle/settings and/or the user"
elog "settings file \$HOME/.isabelle/${MY_P}/etc/settings"
elog "For nitpick it is necessary to install:"
elog "emerge sci-mathematics/kodkodi"
}
sci-mathematics/isabelle/metadata.xml
-29
View File
@@ -1,29 +0,0 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
<pkgmetadata>
<maintainer type="person">
<email>gienah@gentoo.org</email>
</maintainer>
<maintainer type="project">
<email>sci-mathematics@gentoo.org</email>
<name>Gentoo Mathematics Project</name>
</maintainer>
<longdescription lang="en">
Isabelle is a generic proof assistant. It allows mathematical
formulas to be expressed in a formal language and provides tools
for proving those formulas in a logical calculus. The main
application is the formalization of mathematical proofs and in
particular formal verification, which includes proving the
correctness of computer hardware or software and proving
properties of computer languages and protocols.
</longdescription>
<use>
<flag name="graphbrowsing">Generate theory browsing information,
including HTML documents that show a theory's definition, the
theorems proved in its ML file and the relationship with its
ancestors and descendants.</flag>
<flag name="ledit">Use ledit for the isabelle tty line editor</flag>
<flag name="readline">Use readline (rlwrap) for the isabelle tty line
editor</flag>
</use>
</pkgmetadata>