neuper@41945
|
1 |
(* Title: All tests on isac; observe outcommented
|
neuper@41943
|
2 |
Author: Walther Neuper 101001
|
neuper@41943
|
3 |
(c) copyright due to lincense terms.
|
neuper@41943
|
4 |
|
neuper@41943
|
5 |
$ cd /usr/local/isabisac/test/Tools/isac
|
neuper@48884
|
6 |
$ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
|
neuper@41943
|
7 |
*)
|
neuper@41943
|
8 |
|
neuper@52063
|
9 |
theory Test_Isac imports "~~/src/Tools/isac/Build_Isac"
|
neuper@41980
|
10 |
"ADDTESTS/Ctxt"
|
neuper@42048
|
11 |
"ADDTESTS/test-depend/Build_Test"
|
neuper@42023
|
12 |
"ADDTESTS/All_Ctxt"
|
neuper@42179
|
13 |
"ADDTESTS/course/phst11/T1_Basics"
|
neuper@42092
|
14 |
"ADDTESTS/course/phst11/T2_Rewriting"
|
neuper@42179
|
15 |
"ADDTESTS/course/phst11/T3_MathEngine"
|
neuper@42048
|
16 |
"ADDTESTS/file-depend/Build_Test"
|
neuper@42280
|
17 |
"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
|
neuper@42048
|
18 |
"../../Pure/Isar/Test_Parsers"
|
neuper@42048
|
19 |
(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
|
neuper@42048
|
20 |
"../../Pure/Isar/Test_Parse_Term"
|
neuper@42387
|
21 |
|
neuper@41945
|
22 |
uses
|
neuper@41945
|
23 |
( "library.sml")
|
neuper@41945
|
24 |
( "calcelems.sml")
|
neuper@42185
|
25 |
("ProgLang/termC.sml")
|
neuper@41945
|
26 |
("ProgLang/calculate.sml")
|
neuper@41945
|
27 |
("ProgLang/rewrite.sml")
|
neuper@48895
|
28 |
(*"ProgLang/listC.sml"*)
|
akargl@42176
|
29 |
("ProgLang/scrtools.sml")
|
akargl@42176
|
30 |
("ProgLang/tools.sml")
|
neuper@41945
|
31 |
|
neuper@41985
|
32 |
("Minisubpbl/000-comments.sml")
|
neuper@41985
|
33 |
("Minisubpbl/100-init-rootpbl.sml")
|
neuper@41986
|
34 |
("Minisubpbl/150-add-given.sml")
|
neuper@41985
|
35 |
("Minisubpbl/200-start-method.sml")
|
neuper@41985
|
36 |
("Minisubpbl/300-init-subpbl.sml")
|
neuper@41985
|
37 |
("Minisubpbl/400-start-meth-subpbl.sml")
|
neuper@42022
|
38 |
("Minisubpbl/490-nxt-Check_Postcond.sml")
|
neuper@42022
|
39 |
("Minisubpbl/500-met-sub-to-root.sml")
|
neuper@42022
|
40 |
("Minisubpbl/530-error-Check_Elementwise.sml")
|
neuper@42022
|
41 |
("Minisubpbl/600-postcond.sml")
|
neuper@41985
|
42 |
|
neuper@41945
|
43 |
("Interpret/mstools.sml")
|
bonzai@41951
|
44 |
("Interpret/ctree.sml")
|
neuper@41945
|
45 |
("Interpret/ptyps.sml")
|
akargl@42176
|
46 |
("Interpret/generate.sml")
|
neuper@41945
|
47 |
("Interpret/calchead.sml")
|
akargl@42176
|
48 |
("Interpret/appl.sml")
|
neuper@41945
|
49 |
("Interpret/rewtools.sml")
|
akargl@42169
|
50 |
("Interpret/script.sml")
|
akargl@42176
|
51 |
("Interpret/solve.sml")
|
akargl@42176
|
52 |
("Interpret/inform.sml")
|
neuper@41945
|
53 |
("Interpret/mathengine.sml")
|
neuper@41945
|
54 |
|
akargl@42176
|
55 |
("xmlsrc/mathml.sml")
|
neuper@41945
|
56 |
("xmlsrc/datatypes.sml")
|
neuper@41945
|
57 |
("xmlsrc/pbl-met-hierarchy.sml")
|
neuper@48895
|
58 |
(*"xmlsrc/thy-hierarchy.sml"*)
|
neuper@41945
|
59 |
("xmlsrc/interface-xml.sml")
|
neuper@41945
|
60 |
|
neuper@41945
|
61 |
("Frontend/messages.sml")
|
neuper@41945
|
62 |
("Frontend/states.sml")
|
neuper@41945
|
63 |
("Frontend/interface.sml")
|
neuper@41945
|
64 |
("print_exn_G.sml")
|
neuper@41945
|
65 |
|
neuper@41945
|
66 |
("Knowledge/delete.sml")
|
neuper@41945
|
67 |
("Knowledge/descript.sml")
|
neuper@41945
|
68 |
("Knowledge/atools.sml")
|
neuper@41945
|
69 |
("Knowledge/simplify.sml")
|
neuper@41945
|
70 |
("Knowledge/poly.sml")
|
neuper@48884
|
71 |
(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
|
neuper@48884
|
72 |
IN THIS SEQUENCE: SEE Test_Some2.thy*)
|
neuper@48895
|
73 |
(*"Knowledge/rational.sml"*)
|
neuper@41945
|
74 |
("Knowledge/equation.sml")
|
neuper@41945
|
75 |
("Knowledge/root.sml")
|
neuper@41945
|
76 |
("Knowledge/lineq.sml")
|
neuper@48895
|
77 |
(*"Knowledge/rooteq.sml"*)
|
neuper@41945
|
78 |
("Knowledge/rateq.sml")
|
neuper@41945
|
79 |
("Knowledge/rootrateq.sml")
|
neuper@42185
|
80 |
("Knowledge/polyeq.sml")
|
neuper@41945
|
81 |
("Knowledge/calculus.sml")
|
neuper@41945
|
82 |
("Knowledge/trig.sml")
|
neuper@48895
|
83 |
(*"Knowledge/logexp.sml"*)
|
neuper@41945
|
84 |
("Knowledge/diff.sml")
|
neuper@41945
|
85 |
("Knowledge/integrate.sml")
|
neuper@41945
|
86 |
("Knowledge/eqsystem.sml")
|
neuper@41945
|
87 |
("Knowledge/test.sml")
|
neuper@42289
|
88 |
("Knowledge/partial_fractions.sml")
|
neuper@41945
|
89 |
("Knowledge/polyminus.sml")
|
neuper@41945
|
90 |
("Knowledge/vect.sml")
|
neuper@41945
|
91 |
("Knowledge/diffapp.sml")
|
neuper@41945
|
92 |
("Knowledge/biegelinie.sml")
|
neuper@41945
|
93 |
("Knowledge/algein.sml")
|
neuper@41945
|
94 |
("Knowledge/diophanteq.sml")
|
neuper@42412
|
95 |
("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
|
neuper@41945
|
96 |
("Knowledge/isac.sml")
|
neuper@42407
|
97 |
("Knowledge/build_thydata.sml")
|
neuper@41945
|
98 |
|
neuper@41943
|
99 |
begin
|
neuper@48895
|
100 |
section {* test ML Code of isac *}
|
neuper@48895
|
101 |
ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
|
neuper@42179
|
102 |
use "library.sml"
|
neuper@42179
|
103 |
use "calcelems.sml"
|
akargl@42188
|
104 |
use "ProgLang/termC.sml"
|
t@42225
|
105 |
use "ProgLang/calculate.sml"
|
t@42227
|
106 |
use "ProgLang/rewrite.sml"
|
neuper@42185
|
107 |
(*use "ProgLang/listC.sml" 2002*)
|
t@42225
|
108 |
use "ProgLang/scrtools.sml"
|
t@42225
|
109 |
use "ProgLang/tools.sml"
|
neuper@41943
|
110 |
ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41986
|
111 |
ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41985
|
112 |
use "Minisubpbl/000-comments.sml"
|
neuper@41985
|
113 |
use "Minisubpbl/100-init-rootpbl.sml"
|
neuper@41986
|
114 |
use "Minisubpbl/150-add-given.sml"
|
neuper@41985
|
115 |
use "Minisubpbl/200-start-method.sml"
|
neuper@41990
|
116 |
use "Minisubpbl/300-init-subpbl.sml"
|
neuper@41997
|
117 |
use "Minisubpbl/400-start-meth-subpbl.sml"
|
neuper@42022
|
118 |
use "Minisubpbl/490-nxt-Check_Postcond.sml"
|
neuper@41998
|
119 |
use "Minisubpbl/500-met-sub-to-root.sml"
|
neuper@42022
|
120 |
use "Minisubpbl/530-error-Check_Elementwise.sml"
|
neuper@41998
|
121 |
use "Minisubpbl/600-postcond.sml"
|
akargl@42188
|
122 |
ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41943
|
123 |
ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
|
neuper@42185
|
124 |
use "Interpret/mstools.sml"
|
neuper@41989
|
125 |
use "Interpret/ctree.sml" (*!...!see(25)*)
|
neuper@42390
|
126 |
use "Interpret/ptyps.sml"
|
neuper@48891
|
127 |
ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
|
neuper@48895
|
128 |
(*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
|
neuper@42321
|
129 |
use "Interpret/generate.sml"
|
neuper@48895
|
130 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
neuper@48895
|
131 |
... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
|
neuper@48895
|
132 |
use "Interpret/calchead.sml"
|
neuper@48894
|
133 |
use "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
|
neuper@48894
|
134 |
use "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
|
neuper@48895
|
135 |
use "Interpret/script.sml"
|
neuper@48895
|
136 |
use "Interpret/solve.sml"
|
neuper@48895
|
137 |
use "Interpret/inform.sml"
|
neuper@48895
|
138 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
neuper@48895
|
139 |
... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
|
neuper@41972
|
140 |
use "Interpret/mathengine.sml" (*!part.*)
|
neuper@41943
|
141 |
ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41943
|
142 |
ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@48895
|
143 |
use "xmlsrc/mathml.sml" (*part.*)
|
neuper@48895
|
144 |
use "xmlsrc/datatypes.sml" (*TODO/part.*)
|
neuper@48895
|
145 |
use "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
|
neuper@48895
|
146 |
(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
|
neuper@48895
|
147 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
neuper@48895
|
148 |
val it = "----------- ### thes2file ... Exception- Match raised -----------": string
|
neuper@48889
|
149 |
:
|
neuper@48889
|
150 |
val it = "~~~~~ fun thes2file, args:": string
|
neuper@48889
|
151 |
val p = "../../tmp/": path
|
neuper@48889
|
152 |
val it = (): unit
|
neuper@48889
|
153 |
exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")
|
neuper@48889
|
154 |
...CONCERNED WITH thehier
|
neuper@48889
|
155 |
*)
|
akargl@42176
|
156 |
use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
|
neuper@41943
|
157 |
ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41943
|
158 |
ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
|
neuper@42321
|
159 |
use "Frontend/messages.sml"
|
neuper@42321
|
160 |
use "Frontend/states.sml"
|
t@42225
|
161 |
use "Frontend/interface.sml"
|
neuper@48895
|
162 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
neuper@48895
|
163 |
... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
|
neuper@42407
|
164 |
use "print_exn_G.sml"
|
neuper@41943
|
165 |
ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@48895
|
166 |
ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@42321
|
167 |
use "Knowledge/delete.sml"
|
neuper@42321
|
168 |
use "Knowledge/descript.sml"
|
neuper@42397
|
169 |
use "Knowledge/atools.sml"
|
neuper@42396
|
170 |
use "Knowledge/simplify.sml"
|
neuper@42395
|
171 |
use "Knowledge/poly.sml"
|
neuper@48884
|
172 |
(*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
|
neuper@48884
|
173 |
use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
|
neuper@48884
|
174 |
use "Knowledge/gcd_poly_winkler.sml"*)
|
neuper@42399
|
175 |
(*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
|
neuper@42395
|
176 |
use "Knowledge/equation.sml"
|
neuper@42395
|
177 |
use "Knowledge/root.sml"
|
neuper@42395
|
178 |
use "Knowledge/lineq.sml"
|
neuper@42395
|
179 |
(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
|
neuper@42395
|
180 |
use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
|
neuper@42392
|
181 |
use "Knowledge/rootrat.sml"
|
neuper@42397
|
182 |
use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
|
neuper@42289
|
183 |
use "Knowledge/partial_fractions.sml"
|
neuper@42319
|
184 |
use "Knowledge/polyeq.sml"
|
neuper@42413
|
185 |
(*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
|
neuper@42321
|
186 |
use "Knowledge/calculus.sml"
|
t@42225
|
187 |
use "Knowledge/trig.sml"
|
neuper@42393
|
188 |
(*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
|
neuper@42393
|
189 |
use "Knowledge/diff.sml"
|
neuper@42393
|
190 |
use "Knowledge/integrate.sml"
|
neuper@42391
|
191 |
use "Knowledge/eqsystem.sml"
|
t@42225
|
192 |
use "Knowledge/test.sml"
|
neuper@42390
|
193 |
use "Knowledge/polyminus.sml"
|
t@42225
|
194 |
use "Knowledge/vect.sml"
|
neuper@42399
|
195 |
use "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
|
neuper@42387
|
196 |
use "Knowledge/biegelinie.sml"
|
neuper@42385
|
197 |
use "Knowledge/algein.sml"
|
t@42225
|
198 |
use "Knowledge/diophanteq.sml"
|
neuper@42412
|
199 |
use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
|
neuper@42399
|
200 |
use "Knowledge/isac.sml"
|
neuper@42400
|
201 |
use "Knowledge/build_thydata.sml"
|
neuper@48895
|
202 |
ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41945
|
203 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41945
|
204 |
ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
|
neuper@41945
|
205 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
|
neuper@41943
|
206 |
|
neuper@48895
|
207 |
section {* history of tests *}
|
neuper@48895
|
208 |
text {*
|
neuper@48895
|
209 |
Systematic regression tests have been introduced to isac development in 2003.
|
neuper@48895
|
210 |
Sanity of the regression test suffered from updates following Isabelle development,
|
neuper@48895
|
211 |
which mostly exceeded the resources available in isac's development.
|
neuper@48895
|
212 |
|
neuper@48895
|
213 |
The survey below shall support to efficiently use the tests for isac
|
neuper@48895
|
214 |
on different Isabelle versions. Conclusion in most cases will be:
|
neuper@48895
|
215 |
|
neuper@48895
|
216 |
!!! Use most recent tests or go back to the old notebook
|
neuper@48895
|
217 |
with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@48895
|
218 |
*}
|
neuper@48895
|
219 |
|
neuper@48895
|
220 |
subsection {* isac on Isabelle2013 *}
|
neuper@48895
|
221 |
subsubsection {* Summary of development *}
|
neuper@48895
|
222 |
text {*
|
neuper@48895
|
223 |
*}
|
neuper@48895
|
224 |
subsubsection {* Run tests *}
|
neuper@48895
|
225 |
text {*
|
neuper@48895
|
226 |
*}
|
neuper@48895
|
227 |
subsubsection {* State of tests *}
|
neuper@48895
|
228 |
text {*
|
neuper@48895
|
229 |
*}
|
neuper@48895
|
230 |
subsubsection {* Changesets of begin and end *}
|
neuper@48895
|
231 |
text {*
|
neuper@48895
|
232 |
*}
|
neuper@48895
|
233 |
|
neuper@48895
|
234 |
subsection {* isac on Isabelle2012 *}
|
neuper@48895
|
235 |
subsubsection {* Summary of development *}
|
neuper@48895
|
236 |
text {*
|
neuper@48895
|
237 |
isac on Isabelle2012 is considered just a transitional stage
|
neuper@48895
|
238 |
within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
|
neuper@48895
|
239 |
For considerations on the transition see
|
neuper@48895
|
240 |
~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
|
neuper@48895
|
241 |
*}
|
neuper@48895
|
242 |
subsubsection {* Run tests *}
|
neuper@48895
|
243 |
text {*
|
neuper@48895
|
244 |
$ cd /usr/local/isabisac12/
|
neuper@48895
|
245 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
246 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
neuper@48895
|
247 |
*}
|
neuper@48895
|
248 |
subsubsection {* State of tests *}
|
neuper@48895
|
249 |
text {*
|
neuper@48895
|
250 |
At least the tests from isac on Isabelle2011 run again.
|
neuper@48895
|
251 |
However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
|
neuper@48895
|
252 |
in parallel with evaluation.
|
neuper@48895
|
253 |
|
neuper@48895
|
254 |
Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
|
neuper@48895
|
255 |
yields 69 hits, some of which were already present before Isabelle2002-->2009-2
|
neuper@48895
|
256 |
(i.e. on the old notebook from 2002).
|
neuper@48895
|
257 |
|
neuper@48895
|
258 |
Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
|
neuper@48895
|
259 |
# === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
|
neuper@48895
|
260 |
# === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
|
neuper@48895
|
261 |
# === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
|
neuper@48895
|
262 |
Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
|
neuper@48895
|
263 |
|
neuper@48895
|
264 |
Some tests have been re-activated (e.g. error patterns, fill patterns).
|
neuper@48895
|
265 |
*}
|
neuper@48895
|
266 |
subsubsection {* Changesets of begin and end *}
|
neuper@48895
|
267 |
text {*
|
neuper@48895
|
268 |
TODO
|
neuper@48895
|
269 |
:
|
neuper@48895
|
270 |
: isac on Isablle2012
|
neuper@48895
|
271 |
:
|
neuper@48895
|
272 |
Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
|
neuper@48895
|
273 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
274 |
Date: 2012-09-24 18:35:13 +0200 (8 months)
|
neuper@48895
|
275 |
------------------------------------------------------------------------------
|
neuper@48895
|
276 |
Changeset: 48756 (7443906996a8) merged
|
neuper@48895
|
277 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
278 |
Date: 2012-09-24 18:15:49 +0200 (8 months)
|
neuper@48895
|
279 |
*}
|
neuper@48895
|
280 |
|
neuper@48895
|
281 |
subsection {* isac on Isabelle2011 *}
|
neuper@48895
|
282 |
subsubsection {* Summary of development *}
|
neuper@48895
|
283 |
text {*
|
neuper@48895
|
284 |
isac's mathematics engine has been extended by two developments:
|
neuper@48895
|
285 |
(1) Isabelle's contexts were introduced by Mathias Lehnfeld
|
neuper@48895
|
286 |
(2) "error patterns" were introduced by Gabriella Daroczy
|
neuper@48895
|
287 |
Regressions tests have been added for both.
|
neuper@48895
|
288 |
*}
|
neuper@48895
|
289 |
subsubsection {* Run tests *}
|
neuper@48895
|
290 |
text {*
|
neuper@48895
|
291 |
$ cd /usr/local/isabisac11/
|
neuper@48895
|
292 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
293 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
neuper@48895
|
294 |
*}
|
neuper@48895
|
295 |
subsubsection {* State of tests *}
|
neuper@48895
|
296 |
text {*
|
neuper@48895
|
297 |
Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
|
neuper@48895
|
298 |
and sometimes give reasons for failing tests.
|
neuper@48895
|
299 |
(*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
|
neuper@48895
|
300 |
work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
|
neuper@48895
|
301 |
|
neuper@48895
|
302 |
Tests with functions decomposed for single-stepping are marked with
|
neuper@48895
|
303 |
"~~~~~ fun , args:"; val
|
neuper@48895
|
304 |
|
neuper@48895
|
305 |
The most signification tests (in particular Frontend/interface.sml) run,
|
neuper@48895
|
306 |
however, many "error in kernel" are not caught by an exception.
|
neuper@48895
|
307 |
------------------------------------------------------------------------------
|
neuper@48895
|
308 |
After the changeset below Test_Isac worked with check_unsynchronized_ref ():
|
neuper@48895
|
309 |
------------------------------------------------------------------------------
|
neuper@48895
|
310 |
Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
|
neuper@48895
|
311 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
312 |
Date: 2012-08-06 10:38:11 +0200 (11 months)
|
neuper@48895
|
313 |
*}
|
neuper@48895
|
314 |
subsubsection {* Changesets of begin and end *}
|
neuper@48895
|
315 |
text {*
|
neuper@48895
|
316 |
isac development was done between these changesets:
|
neuper@48895
|
317 |
------------------------------------------------------------------------------
|
neuper@48895
|
318 |
Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
|
neuper@48895
|
319 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
320 |
Date: 2012-09-24 16:39:30 +0200 (8 months)
|
neuper@48895
|
321 |
:
|
neuper@48895
|
322 |
: isac on Isablle2011
|
neuper@48895
|
323 |
:
|
neuper@48895
|
324 |
Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
|
neuper@48895
|
325 |
Branch: decompose-isar
|
neuper@48895
|
326 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
327 |
Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
|
neuper@48895
|
328 |
------------------------------------------------------------------------------
|
neuper@48895
|
329 |
*}
|
neuper@48895
|
330 |
|
neuper@48895
|
331 |
subsection {* isac on Isabelle2009-2 *}
|
neuper@48895
|
332 |
subsubsection {* Summary of development *}
|
neuper@48895
|
333 |
text {*
|
neuper@48895
|
334 |
In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
|
neuper@48895
|
335 |
The update was painful (bridging 7 years of Isabelle development) and cut short
|
neuper@48895
|
336 |
due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
|
neuper@48895
|
337 |
going on to Isabelle2011 although most of the tests did not run.
|
neuper@48895
|
338 |
*}
|
neuper@48895
|
339 |
subsubsection {* Run tests *}
|
neuper@48895
|
340 |
text {*
|
neuper@48895
|
341 |
$ cd /usr/local/isabisac09-2/
|
neuper@48895
|
342 |
$ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
343 |
$ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
|
neuper@48895
|
344 |
NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
|
neuper@48895
|
345 |
*}
|
neuper@48895
|
346 |
subsubsection {* State of tests *}
|
neuper@48895
|
347 |
text {*
|
neuper@48895
|
348 |
Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
|
neuper@48895
|
349 |
If really necessary, go back to the old notebook with Isabelle2002.
|
neuper@48895
|
350 |
*}
|
neuper@48895
|
351 |
subsubsection {* Changesets of begin and end *}
|
neuper@48895
|
352 |
text {*
|
neuper@48895
|
353 |
isac development was done between these changesets:
|
neuper@48895
|
354 |
------------------------------------------------------------------------------
|
neuper@48895
|
355 |
Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
|
neuper@48895
|
356 |
Branch: decompose-isar
|
neuper@48895
|
357 |
User: Marco Steger <m.steger@student.tugraz.at>
|
neuper@48895
|
358 |
Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
|
neuper@48895
|
359 |
:
|
neuper@48895
|
360 |
: isac on Isablle2009-2
|
neuper@48895
|
361 |
:
|
neuper@48895
|
362 |
Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
|
neuper@48895
|
363 |
Branch: isac-from-Isabelle2009-2
|
neuper@48895
|
364 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
365 |
Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
|
neuper@48895
|
366 |
------------------------------------------------------------------------------
|
neuper@48895
|
367 |
*}
|
neuper@48895
|
368 |
|
neuper@48895
|
369 |
subsection {* isac on Isabelle2002 *}
|
neuper@48895
|
370 |
subsubsection {* Summary of development *}
|
neuper@48895
|
371 |
text {*
|
neuper@48895
|
372 |
From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
|
neuper@48895
|
373 |
of isac's mathematics engine has been implemented.
|
neuper@48895
|
374 |
*}
|
neuper@48895
|
375 |
subsubsection {* Run tests *}
|
neuper@48895
|
376 |
subsubsection {* State of tests *}
|
neuper@48895
|
377 |
text {*
|
neuper@48895
|
378 |
All tests work on an old notebook (the right PolyML coudn't be upgraded to more
|
neuper@48895
|
379 |
recent Linux versions)
|
neuper@48895
|
380 |
*}
|
neuper@48895
|
381 |
subsubsection {* Changesets of begin and end *}
|
neuper@48895
|
382 |
text {*
|
neuper@48895
|
383 |
Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
|
neuper@48895
|
384 |
see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
|
neuper@48895
|
385 |
*}
|
neuper@48895
|
386 |
|
neuper@41943
|
387 |
end
|
neuper@42067
|
388 |
(*========== inhibit exn 110628 ================================================
|
neuper@42067
|
389 |
============ inhibit exn 110628 ==============================================*)
|
neuper@41943
|
390 |
|
neuper@41943
|
391 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@48895
|
392 |
Pending source file dependencies: "Knowledge/algein.sml"
|
neuper@48895
|
393 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
neuper@41975
|
394 |
|