Gentoo Archives: gentoo-commits

From: "Mark Wright (gienah)" <gienah@g.o>
To: gentoo-commits@l.g.o
Subject: [gentoo-commits] gentoo-x86 commit in sci-mathematics/isabelle/files: isabelle-2013-classpath.patch isabelle-2013-gentoo-settings.patch isabelle-2013-HOL-Predicate_Compile_Examples.patch
Date: Sat, 31 Aug 2013 09:24:19
Message-Id: 20130831092413.3D2FC2004B@flycatcher.gentoo.org
1 gienah 13/08/31 09:24:13
2
3 Added: isabelle-2013-classpath.patch
4 isabelle-2013-gentoo-settings.patch
5 isabelle-2013-HOL-Predicate_Compile_Examples.patch
6 Log:
7 Bump isabelle to 2013, fixes bug 468344
8
9 (Portage version: 2.2.1/cvs/Linux x86_64, signed Manifest commit with key 618E971F)
10
11 Revision Changes Path
12 1.1 sci-mathematics/isabelle/files/isabelle-2013-classpath.patch
13
14 file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch?rev=1.1&view=markup
15 plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-classpath.patch?rev=1.1&content-type=text/plain
16
17 Index: isabelle-2013-classpath.patch
18 ===================================================================
19 --- Isabelle2013-orig/lib/Tools/java 2013-02-13 00:31:02.000000000 +1100
20 +++ Isabelle2013/lib/Tools/java 2013-08-18 14:07:51.704133000 +1000
21 @@ -6,5 +6,5 @@
22
23 CLASSPATH="$(jvmpath "$CLASSPATH")"
24 isabelle_jdk java -Dfile.encoding=UTF-8 -server \
25 - "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
26 + "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
27
28 --- Isabelle2013-orig/lib/Tools/scala 2013-02-13 00:31:02.000000000 +1100
29 +++ Isabelle2013/lib/Tools/scala 2013-08-18 14:07:00.795248000 +1000
30 @@ -8,4 +8,4 @@
31
32 CLASSPATH="$(jvmpath "$CLASSPATH")"
33 isabelle_scala scala -Dfile.encoding=UTF-8 \
34 - "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
35 + "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
36 --- Isabelle2013-orig/lib/Tools/scalac 2013-02-13 00:31:02.000000000 +1100
37 +++ Isabelle2013/lib/Tools/scalac 2013-08-18 14:07:32.751448000 +1000
38 @@ -8,5 +8,5 @@
39
40 CLASSPATH="$(jvmpath "$CLASSPATH")"
41 isabelle_scala scalac -Dfile.encoding=UTF-8 \
42 - "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
43 + "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext:$(java-config -p scala | sed 's@\([^:]*\)/[^:]*:.*@\1@')")" "$@"
44
45 --- Isabelle2013-orig/src/Pure/build-jars 2013-02-13 00:31:15.000000000 +1100
46 +++ Isabelle2013/src/Pure/build-jars 2013-08-18 12:55:51.400924000 +1000
47 @@ -133,7 +133,7 @@
48 declare -a JFREECHART_JARS=()
49 for NAME in $JFREECHART_JAR_NAMES
50 do
51 - JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
52 + JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
53 done
54
55
56 --- Isabelle2013-orig/src/Tools/jEdit/lib/Tools/jedit 2013-02-13 00:31:16.000000000 +1100
57 +++ Isabelle2013/src/Tools/jEdit/lib/Tools/jedit 2013-08-18 16:39:15.495244000 +1000
58 @@ -214,97 +214,11 @@
59 declare -a JFREECHART_JARS=()
60 for NAME in $JFREECHART_JAR_NAMES
61 do
62 - JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
63 + JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$NAME"
64 done
65
66 -
67 -# target
68 -
69 -TARGET="dist/jars/Isabelle-jEdit.jar"
70 -
71 -declare -a UPDATED=()
72 -
73 -if [ "$BUILD_JARS" = jars_fresh ]; then
74 - OUTDATED=true
75 -else
76 - OUTDATED=false
77 - if [ ! -e "$TARGET" ]; then
78 - OUTDATED=true
79 - else
80 - if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
81 - declare -a DEPS=(
82 - "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}"
83 - "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
84 - )
85 - elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
86 - declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
87 - else
88 - declare -a DEPS=()
89 - fi
90 - for DEP in "${DEPS[@]}"
91 - do
92 - [ ! -e "$DEP" ] && fail "Missing file: $DEP"
93 - [ "$DEP" -nt "$TARGET" ] && {
94 - OUTDATED=true
95 - UPDATED["${#UPDATED[@]}"]="$DEP"
96 - }
97 - done
98 - fi
99 -fi
100 -
101 -
102 -# build
103 -
104 -if [ "$OUTDATED" = true ]
105 -then
106 - echo "### Building Isabelle/jEdit ..."
107 -
108 - [ "${#UPDATED[@]}" -gt 0 ] && {
109 - echo "Changed files:"
110 - for FILE in "${UPDATED[@]}"
111 - do
112 - echo " $FILE"
113 - done
114 - }
115 -
116 - [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
117 - fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
118 -
119 - rm -rf dist || failed
120 - mkdir -p dist dist/classes || failed
121 -
122 - cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
123 - cp -p -R -f "${RESOURCES[@]}" dist/classes/.
124 - cp src/jEdit.props dist/properties/.
125 - cp -p -R -f src/modes/. dist/modes/.
126 -
127 - perl -i -e 'while (<>) {
128 - if (m/NAME="javacc"/) {
129 - print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
130 - print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
131 - print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
132 - print; }' dist/modes/catalog
133 -
134 - cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
135 - (
136 - for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \
137 - "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
138 - do
139 - CLASSPATH="$CLASSPATH:$JAR"
140 - done
141 - CLASSPATH="$(jvmpath "$CLASSPATH")"
142 - exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
143 - ) || fail "Failed to compile sources"
144 -
145 - cd dist/classes
146 - isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
147 - cd ../..
148 - rm -rf dist/classes
149 -fi
150 -
151 popd >/dev/null
152
153 -
154 ## main
155
156 if [ "$BUILD_ONLY" = false ]; then
157 --- Isabelle2013-orig/contrib/jfreechart-1.0.14/etc/settings 2012-12-09 07:23:53.000000000 +1100
158 +++ Isabelle2013/contrib/jfreechart-1.0.14/etc/settings 2013-08-18 16:18:10.244698000 +1000
159 @@ -1,7 +1,5 @@
160 # -*- shell-script -*- :mode=shellscript:
161
162 JFREECHART_HOME="$COMPONENT"
163 -JFREECHART_JAR_NAMES="iText-2.1.5.jar jcommon-1.0.18.jar jfreechart-1.0.14.jar"
164 -
165 -ISABELLE_JAVA_EXT="$ISABELLE_JAVA_EXT:$JFREECHART_HOME/lib"
166 +JFREECHART_JAR_NAMES="$(java-config -p itext | sed -e 's@:@ @g') $(java-config -p jcommon-1.0 | sed -e 's@:@ @g') $(java-config -p jfreechart-1.0 | sed -e 's@:@ @g')"
167
168
169
170
171 1.1 sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch
172
173 file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch?rev=1.1&view=markup
174 plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-gentoo-settings.patch?rev=1.1&content-type=text/plain
175
176 Index: isabelle-2013-gentoo-settings.patch
177 ===================================================================
178 --- Isabelle2013-orig/etc/settings 2013-02-13 00:31:02.000000000 +1100
179 +++ Isabelle2013/etc/settings 2013-08-17 14:47:46.045988000 +1000
180 @@ -176,3 +176,16 @@
181 #ISABELLE_GHC="/usr/bin/ghc"
182 #ISABELLE_OCAML="/usr/bin/ocaml"
183 #ISABELLE_SWIPL="/usr/bin/swipl"
184 +
185 +# Poly/ML Gentoo (x86_64)
186 +ML_PLATFORM=x86_64-linux
187 +ML_HOME="/usr/bin"
188 +ML_SYSTEM=polyml-5.5.0
189 +ML_OPTIONS="-H 1000"
190 +ML_SOURCES="/usr/src/debug/dev-lang/polyml-5.5.0"
191 +
192 +# Proof General home
193 +PROOFGENERAL_HOME="/usr/share/emacs/site-lisp/ProofGeneral"
194 +PROOFGENERAL_OPTIONS=""
195 +#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
196 +
197
198
199
200 1.1 sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch
201
202 file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch?rev=1.1&view=markup
203 plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/isabelle/files/isabelle-2013-HOL-Predicate_Compile_Examples.patch?rev=1.1&content-type=text/plain
204
205 Index: isabelle-2013-HOL-Predicate_Compile_Examples.patch
206 ===================================================================
207 --- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-02-13 00:31:10.000000000 +1100
208 +++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy 2013-08-31 14:37:02.015159000 +1000
209 @@ -82,7 +82,7 @@
210 setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
211
212 lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
213 -quickcheck[tester = prolog, iterations = 1, expect = counterexample]
214 +quickcheck[tester = prolog, iterations = 1]
215 oops
216
217 section {* Manual setup to find the counterexample *}
218 @@ -110,7 +110,7 @@
219
220 lemma
221 "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
222 -quickcheck[tester = prolog, iterations = 1, expect = counterexample]
223 +quickcheck[tester = prolog, iterations = 1]
224 oops
225
226 section {* Using a global limit for limiting the execution *}
227 @@ -146,7 +146,7 @@
228
229 lemma
230 "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
231 -quickcheck[tester = prolog, iterations = 1, expect = counterexample]
232 +quickcheck[tester = prolog, iterations = 1]
233 oops
234
235 end
236 \ No newline at end of file
237 --- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-02-13 00:31:10.000000000 +1100
238 +++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 2013-08-31 14:36:47.049851000 +1000
239 @@ -33,7 +33,7 @@
240
241 lemma
242 "S\<^isub>1p w \<Longrightarrow> w = []"
243 -quickcheck[tester = prolog, iterations=1, expect = counterexample]
244 +quickcheck[tester = prolog, iterations=1]
245 oops
246
247 definition "filter_a = filter (\<lambda>x. x = a)"
248 @@ -67,7 +67,7 @@
249
250 theorem S\<^isub>1_sound:
251 "S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
252 -quickcheck[tester = prolog, iterations=1, expect = counterexample]
253 +quickcheck[tester = prolog, iterations=1]
254 oops
255
256
257 @@ -91,7 +91,7 @@
258
259 theorem S\<^isub>2_sound:
260 "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
261 -quickcheck[tester = prolog, iterations=1, expect = counterexample]
262 +quickcheck[tester = prolog, iterations=1]
263 oops
264
265 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
266 --- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-02-13 00:31:10.000000000 +1100
267 +++ Isabelle2013/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy 2013-08-31 14:28:11.784390000 +1000
268 @@ -92,7 +92,7 @@
269
270 lemma
271 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
272 -quickcheck[tester = prolog, iterations = 1, expect = counterexample]
273 +quickcheck[tester = prolog, iterations = 1]
274 oops
275
276 text {* Verifying that the found counterexample really is one by means of a proof *}
277 --- Isabelle2013-orig/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-02-13 00:31:10.000000000 +1100
278 +++ Isabelle2013/src/HOL/Predicate_Compile_Examples/List_Examples.thy 2013-08-31 14:27:52.013962000 +1000
279 @@ -21,7 +21,7 @@
280 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
281 quickcheck[tester = random, iterations = 10000]
282 quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
283 -quickcheck[tester = prolog, expect = counterexample]
284 +quickcheck[tester = prolog]
285 oops
286
287 end
288 \ No newline at end of file