diff options
Diffstat (limited to 'sci-mathematics/isabelle/files')
10 files changed, 0 insertions, 280 deletions
diff --git a/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch b/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch deleted file mode 100644 index 3e63f1c62237..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2012-graphbrowser.patch +++ /dev/null @@ -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 - diff --git a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch b/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch deleted file mode 100644 index 233ea5b50fad..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2012-reverse-line-editor-order.patch +++ /dev/null @@ -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)" - - - ### diff --git a/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch deleted file mode 100644 index 032b18b71f3b..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016-classpath.patch +++ /dev/null @@ -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)")" "$@" - diff --git a/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch deleted file mode 100644 index 9a88ebef26ca..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016-jfreechart-classpath.patch +++ /dev/null @@ -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)" diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch deleted file mode 100644 index 38d047199ce8..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-bash_process-1.2.1-settings.patch +++ /dev/null @@ -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" diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch deleted file mode 100644 index 6bac5ccbe748..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-disable-jedit-build-after-install.patch +++ /dev/null @@ -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 - - diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch deleted file mode 100644 index a34cae3fcf45..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-jortho-1.0-2-classpath.patch +++ /dev/null @@ -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)" diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch deleted file mode 100644 index f19436acd1c3..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-libsha1.patch +++ /dev/null @@ -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 => diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch deleted file mode 100644 index d766a957021d..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_read_only_certificates.patch +++ /dev/null @@ -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. diff --git a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch b/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch deleted file mode 100644 index 249c94bd2583..000000000000 --- a/sci-mathematics/isabelle/files/isabelle-2016.1-smt_timeout.patch +++ /dev/null @@ -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) |