gienah 15/01/25 13:08:28
Added: isabelle-2013.2-classpath.patch
isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
Log:
Bump isabelle to 2013.2. Fix Bug 536324 - sci-mathematics/isabelle: Slot
dependencies for java packages. Add upper range dependency
<dev-lang/scala-2.11.1 to 2013-r1.
(Portage version: 2.2.15/cvs/Linux x86_64, signed Manifest commit with key
618E971F)
Revision Changes Path
1.1
sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch
file :
http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch?rev=1.1&view=markup
plain:
http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013.2-classpath.patch?rev=1.1&content-type=text/plain
Index: isabelle-2013.2-classpath.patch
===================================================================
--- Isabelle2013-2-orig/lib/Tools/java 2013-12-06 02:18:34.000000000 +1100
+++ Isabelle2013-2/lib/Tools/java 2014-02-09 20:53:30.085279943 +1100
@@ -10,5 +10,5 @@
unset CLASSPATH
isabelle_jdk java "${JAVA_ARGS[@]}" \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala | sed
's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/lib/Tools/scala 2013-12-06 02:18:34.000000000 +1100
+++ Isabelle2013-2/lib/Tools/scala 2014-02-09 20:54:22.418737591 +1100
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scala -Dfile.encoding=UTF-8 \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala | sed
's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/lib/Tools/scalac 2013-12-06 02:18:34.000000000
+1100
+++ Isabelle2013-2/lib/Tools/scalac 2014-02-09 20:55:03.999895037 +1100
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(jvmpath "$ISABELLE_CLASSPATH:$(java-config -p scala | sed
's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
--- Isabelle2013-2-orig/src/Tools/jEdit/lib/Tools/jedit 2013-12-06
02:19:04.000000000 +1100
+++ Isabelle2013-2/src/Tools/jEdit/lib/Tools/jedit 2014-02-09
20:59:14.026841490 +1100
@@ -211,105 +211,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" "$GRAPHVIEW_JAR"
- "${SOURCES[@]}" "${RESOURCES[@]}"
- )
- elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_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/NAME="javacc"/) {
- print qq,<MODE NAME="isabelle" FILE="isabelle.xml"
FILE_NAME_GLOB="*.thy"/>\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; }' dist/modes/catalog
-
- cd dist
- isabelle_jdk jar xf jedit.jar
- cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
- "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
- cp "$ISABELLE_HOME/lib/logo/isabelle-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
- (
- #workaround for scalac 2.10.2
- function stty() { :; }
- export -f stty
-
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
- do
- classpath "$JAR"
- done
- export CLASSPATH="$(jvmpath "$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
-fi
-
popd >/dev/null
1.1
sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
file :
http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch?rev=1.1&view=markup
plain:
http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013.2-HOL-Predicate_Compile_Examples.patch?rev=1.1&content-type=text/plain
Index: isabelle-2013.2-HOL-Predicate_Compile_Examples.patch
===================================================================
---
Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
2013-12-06 02:18:50.000000000 +1100
+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
2014-02-09 22:21:20.676081140 +1100
@@ -87,7 +87,7 @@
*}
lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r =
Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
section {* Manual setup to find the counterexample *}
@@ -115,7 +115,7 @@
lemma
"hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
section {* Using a global limit for limiting the execution *}
@@ -151,7 +151,7 @@
lemma
"hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
end
\ No newline at end of file
---
Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
2013-12-06 02:18:50.000000000 +1100
+++
Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
2014-02-09 22:27:26.826238011 +1100
@@ -36,7 +36,7 @@
lemma
"S\<^sub>1p w \<Longrightarrow> w = []"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
definition "filter_a = filter (\<lambda>x. x = a)"
@@ -70,7 +70,7 @@
theorem S\<^sub>1_sound:
"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x
\<leftarrow> w. x = b]"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
@@ -94,7 +94,7 @@
theorem S\<^sub>2_sound:
"S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x
\<leftarrow> w. x = b]"
-quickcheck[tester = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1]
oops
inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
@@ -171,4 +171,4 @@
hide_const a b
-end
\ No newline at end of file
+end
--- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
2013-12-06 02:18:50.000000000 +1100
+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
2014-02-09 22:21:20.677081168 +1100
@@ -95,7 +95,7 @@
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta>
t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1]
oops
text {* Verifying that the found counterexample really is one by means of a
proof *}
--- Isabelle2013-2-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy
2013-12-06 02:18:50.000000000 +1100
+++ Isabelle2013-2/src/HOL/Predicate_Compile_Examples/List_Examples.thy
2014-02-09 22:21:20.678081196 +1100
@@ -24,7 +24,7 @@
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
quickcheck[tester = random, iterations = 10000]
quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
-quickcheck[tester = prolog, expect = counterexample]
+quickcheck[tester = prolog]
oops
end
\ No newline at end of file
