neuper@52065
|
1 |
(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
|
neuper@41943
|
2 |
Author: Walther Neuper 101001
|
wneuper@59258
|
3 |
(c) copyright due to license terms.
|
neuper@41943
|
4 |
|
neuper@52101
|
5 |
Isac's tests are organised parallel to sources:
|
neuper@52101
|
6 |
"~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
|
neuper@52101
|
7 |
plus
|
neuper@52065
|
8 |
~~/test/Tools/isac/ADDTESTS
|
neuper@52101
|
9 |
~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
|
wneuper@59323
|
10 |
-------------------------------------------------------------------------------
|
neuper@52065
|
11 |
|
wneuper@59323
|
12 |
Prepare running tests: see below
|
wneuper@59323
|
13 |
Run tests:
|
neuper@52065
|
14 |
$ cd /usr/local/isabisac/
|
wneuper@59323
|
15 |
$ export ISABELLE_VERSION=2015 # for libisabelle
|
neuper@52065
|
16 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
|
neuper@41943
|
17 |
*)
|
neuper@41943
|
18 |
|
wneuper@59258
|
19 |
section \<open>Prepare running tests\<close>
|
wneuper@59258
|
20 |
text \<open>
|
wneuper@59323
|
21 |
Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
|
wneuper@59258
|
22 |
This policy conflicts with those tests, which go into functions to details
|
wneuper@59258
|
23 |
not declared in the signatures.
|
wneuper@59258
|
24 |
|
wneuper@59258
|
25 |
In order to maintain these tests without changes, this has to be done before running tests:
|
wneuper@59323
|
26 |
(1) Extend signatures for tests by
|
wneuper@59323
|
27 |
~~$ ./xcoding-to-test.sh
|
wneuper@59323
|
28 |
~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
|
wneuper@59323
|
29 |
Running Test_Isac.thy opens all structures, see code after "begin" below.
|
wneuper@59323
|
30 |
(2) Clean signatures for coding
|
wneuper@59323
|
31 |
~~$ ./xtest-to-coding.sh
|
wneuper@59323
|
32 |
~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
|
wneuper@59323
|
33 |
|
wneuper@59323
|
34 |
********************* don't forget (2) BEFORE pushing to repository *********************
|
wneuper@59323
|
35 |
|
wneuper@59323
|
36 |
The above bash files accomplish query replace in src/Tools/isac:
|
wneuper@59261
|
37 |
\<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
|
wneuper@59261
|
38 |
\<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
|
wneuper@59261
|
39 |
^^^ in signature outcommented, ^^^ NOT outcommented,
|
wneuper@59261
|
40 |
this is status for coding this is status for tests
|
wneuper@59258
|
41 |
\<close>
|
wneuper@59258
|
42 |
|
wneuper@59366
|
43 |
section \<open>code for copy & paste\<close>
|
wneuper@59366
|
44 |
text \<open>
|
wneuper@59366
|
45 |
"~~~~~ fun , args:"; val () = ();
|
wneuper@59366
|
46 |
"~~~~~ and , args:"; val () = ();
|
wneuper@59565
|
47 |
"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
|
wneuper@59366
|
48 |
|
wneuper@59366
|
49 |
\<close>
|
wneuper@59258
|
50 |
section \<open>Run the tests\<close>
|
wneuper@59258
|
51 |
text \<open>
|
wneuper@59258
|
52 |
* say "OK" to the popup asking for theories to be loaded
|
wneuper@59258
|
53 |
* watch the <Theories> window for errors in the "imports" below
|
wneuper@59258
|
54 |
\<close>
|
neuper@52073
|
55 |
|
wneuper@59468
|
56 |
theory Test_Isac
|
wneuper@59465
|
57 |
imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
|
wneuper@59465
|
58 |
(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
|
neuper@52116
|
59 |
"ADDTESTS/accumulate-val/Thy_All"
|
neuper@41980
|
60 |
"ADDTESTS/Ctxt"
|
neuper@42048
|
61 |
"ADDTESTS/test-depend/Build_Test"
|
neuper@42023
|
62 |
"ADDTESTS/All_Ctxt"
|
wneuper@59202
|
63 |
"ADDTESTS/Test_Units"
|
neuper@42179
|
64 |
"ADDTESTS/course/phst11/T1_Basics"
|
neuper@42092
|
65 |
"ADDTESTS/course/phst11/T2_Rewriting"
|
neuper@42179
|
66 |
"ADDTESTS/course/phst11/T3_MathEngine"
|
neuper@52065
|
67 |
"ADDTESTS/file-depend/BuildC_Test"
|
neuper@52102
|
68 |
"ADDTESTS/session-get_theory/Foo"
|
wneuper@59144
|
69 |
(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
|
wneuper@59144
|
70 |
ADDTESTS/------------------------------------------- see end of tests *)
|
wneuper@59194
|
71 |
(*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
|
neuper@52089
|
72 |
(*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
|
neuper@52073
|
73 |
"~~/test/Pure/Isar/Test_Parse_Term"
|
wneuper@59364
|
74 |
(*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
|
neuper@55364
|
75 |
"~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
|
neuper@55366
|
76 |
"~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
|
wneuper@59388
|
77 |
|
wneuper@59388
|
78 |
|
wneuper@59388
|
79 |
|
wneuper@59362
|
80 |
"~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
|
s1210629013@55377
|
81 |
"~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
|
wneuper@59364
|
82 |
(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
|
neuper@52168
|
83 |
"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
|
neuper@52168
|
84 |
"~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
|
wneuper@59364
|
85 |
(*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
|
neuper@52168
|
86 |
|
neuper@41943
|
87 |
begin
|
s1210629013@55442
|
88 |
|
wneuper@59472
|
89 |
ML \<open>
|
wneuper@59258
|
90 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
|
wneuper@59318
|
91 |
(* these vvv test, if funs are intermediately opened in structure
|
wneuper@59318
|
92 |
in case of errors here consider ~~/./xtest-to-coding.sh *)
|
wneuper@59261
|
93 |
open Kernel;
|
wneuper@59262
|
94 |
open Math_Engine; CalcTreeTEST;
|
wneuper@59559
|
95 |
open Lucin; itms2args;
|
wneuper@59559
|
96 |
open LucinNEW; appy;
|
wneuper@59600
|
97 |
open Istate;
|
wneuper@59262
|
98 |
open Inform; cas_input;
|
wneuper@59263
|
99 |
open Rtools; trtas2str;
|
wneuper@59265
|
100 |
open Chead; pt_extract;
|
wneuper@59316
|
101 |
open Generate; (* NONE *)
|
wneuper@59276
|
102 |
open Ctree; append_problem;
|
wneuper@59601
|
103 |
open Prog_Tac;
|
walther@59603
|
104 |
open Tactical;
|
walther@59603
|
105 |
open Prog_Expr;
|
walther@59603
|
106 |
(*open Auto_Prog;*)
|
walther@59617
|
107 |
open Input_Descript;
|
wneuper@59269
|
108 |
open Specify; show_ptyps;
|
wneuper@59316
|
109 |
open Applicable; mk_set;
|
wneuper@59316
|
110 |
open Solve; (* NONE *)
|
wneuper@59299
|
111 |
open Selem; e_fmz;
|
wneuper@59577
|
112 |
open Stool; (* NONE *)
|
wneuper@59577
|
113 |
open ContextC; transfer_asms_from_to;
|
wneuper@59571
|
114 |
open Tactic; (* NONE *)
|
wneuper@59316
|
115 |
open Model; (* NONE *)
|
wneuper@59384
|
116 |
open LTool; rule2stac;
|
wneuper@59384
|
117 |
open Rewrite; mk_thm;
|
wneuper@59388
|
118 |
open Calc; get_pair;
|
wneuper@59410
|
119 |
open TermC; atomt;
|
wneuper@59417
|
120 |
open Celem; e_pbt;
|
wneuper@59417
|
121 |
open Rule; string_of_thm;
|
wneuper@59258
|
122 |
(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59472
|
123 |
\<close>
|
wneuper@59366
|
124 |
|
wneuper@59462
|
125 |
ML \<open>
|
wneuper@59366
|
126 |
"~~~~~ fun xxx, args:"; val () = ();
|
wneuper@59462
|
127 |
\<close> ML \<open>
|
wneuper@59462
|
128 |
\<close> ML \<open>
|
wneuper@59462
|
129 |
\<close>
|
wneuper@59356
|
130 |
|
wneuper@59472
|
131 |
ML \<open>
|
s1210629013@55446
|
132 |
KEStore_Elems.set_ref_thy @{theory};
|
wneuper@59248
|
133 |
(*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
|
wneuper@59472
|
134 |
\<close>
|
s1210629013@55442
|
135 |
|
wneuper@59372
|
136 |
(*---------------------- check test file by testfile -------------------------------------------
|
wneuper@59372
|
137 |
---------------------- check test file by testfile -------------------------------------------*)
|
wneuper@59472
|
138 |
section \<open>trials with Isabelle's functions\<close>
|
wneuper@59472
|
139 |
ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
neuper@52119
|
140 |
ML_file "~~/test/Pure/General/alist.ML"
|
neuper@52119
|
141 |
ML_file "~~/test/Pure/General/basics.ML"
|
neuper@52119
|
142 |
ML_file "~~/test/Pure/General/scan.ML"
|
wneuper@59115
|
143 |
ML_file "~~/test/Pure/PIDE/xml.ML"
|
wneuper@59472
|
144 |
ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
neuper@52119
|
145 |
|
wneuper@59472
|
146 |
section \<open>test ML Code of isac\<close>
|
wneuper@59600
|
147 |
subsection \<open>basic code first\<close>
|
wneuper@59472
|
148 |
ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59594
|
149 |
ML_file "CalcElements/libraryC.sml"
|
wneuper@59594
|
150 |
ML_file "CalcElements/calcelems.sml"
|
wneuper@59356
|
151 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59388
|
152 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
wneuper@59594
|
153 |
ML_file "CalcElements/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
|
wneuper@59594
|
154 |
ML_file "CalcElements/termC.sml"
|
wneuper@59594
|
155 |
ML_file "CalcElements/listC.sml"
|
wneuper@59594
|
156 |
ML_file "CalcElements/contextC.sml"
|
wneuper@59359
|
157 |
ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
|
wneuper@59358
|
158 |
ML_file "ProgLang/rewrite.sml"
|
neuper@52065
|
159 |
ML_file "ProgLang/scrtools.sml"
|
neuper@52065
|
160 |
ML_file "ProgLang/tools.sml"
|
wneuper@59362
|
161 |
(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
|
wneuper@59366
|
162 |
---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
|
wneuper@59600
|
163 |
|
wneuper@59600
|
164 |
subsection \<open>basic functionality on simple example first\<close>
|
neuper@52065
|
165 |
ML_file "Minisubpbl/000-comments.sml"
|
neuper@52065
|
166 |
ML_file "Minisubpbl/100-init-rootpbl.sml"
|
neuper@52065
|
167 |
ML_file "Minisubpbl/150-add-given.sml"
|
neuper@52065
|
168 |
ML_file "Minisubpbl/200-start-method.sml"
|
wneuper@59411
|
169 |
ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
|
neuper@52065
|
170 |
ML_file "Minisubpbl/300-init-subpbl.sml"
|
neuper@52065
|
171 |
ML_file "Minisubpbl/400-start-meth-subpbl.sml"
|
wneuper@59492
|
172 |
ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
|
neuper@52065
|
173 |
ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
|
neuper@52065
|
174 |
ML_file "Minisubpbl/500-met-sub-to-root.sml"
|
neuper@52065
|
175 |
ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
|
neuper@52065
|
176 |
ML_file "Minisubpbl/600-postcond.sml"
|
wneuper@59493
|
177 |
ML_file "Minisubpbl/700-interSteps.sml"
|
wneuper@59569
|
178 |
ML_file "Minisubpbl/799-complete.sml"
|
wneuper@59600
|
179 |
|
wneuper@59600
|
180 |
subsection \<open>further functionality alongside batch build sequence\<close>
|
wneuper@59594
|
181 |
ML_file "Specify/mstools.sml"
|
wneuper@59594
|
182 |
ML_file "Specify/specification-elems.sml"
|
wneuper@59594
|
183 |
ML_file "Specify/ctree.sml" (*!...!see(25)*)
|
wneuper@59594
|
184 |
ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
|
wneuper@59472
|
185 |
ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
|
wneuper@59594
|
186 |
ML_file "Specify/generate.sml"
|
wneuper@59594
|
187 |
ML_file "Specify/calchead.sml"
|
wneuper@59594
|
188 |
ML_file "Specify/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
|
wneuper@59600
|
189 |
|
wneuper@55498
|
190 |
ML_file "Interpret/rewtools.sml"
|
neuper@52065
|
191 |
ML_file "Interpret/script.sml"
|
wneuper@59561
|
192 |
ML_file "Interpret/inform.sml"
|
wneuper@59561
|
193 |
ML_file "Interpret/lucas-interpreter.sml"
|
wneuper@59600
|
194 |
|
wneuper@59600
|
195 |
ML_file "MathEngine/solve.sml"
|
wneuper@59600
|
196 |
ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
|
wneuper@59600
|
197 |
ML_file "MathEngine/messages.sml"
|
wneuper@59600
|
198 |
ML_file "MathEngine/states.sml"
|
wneuper@59600
|
199 |
|
wneuper@59600
|
200 |
ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
|
wneuper@59600
|
201 |
ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
|
wneuper@59600
|
202 |
ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
|
wneuper@59600
|
203 |
ML_file "BridgeLibisabelle/thy-hierarchy.sml"
|
wneuper@59600
|
204 |
ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
|
wneuper@59600
|
205 |
ML_file "BridgeLibisabelle/interface.sml"
|
neuper@48895
|
206 |
(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
|
neuper@48895
|
207 |
... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
|
wneuper@59600
|
208 |
|
neuper@52065
|
209 |
ML_file "Knowledge/delete.sml"
|
neuper@52065
|
210 |
ML_file "Knowledge/descript.sml"
|
neuper@52065
|
211 |
ML_file "Knowledge/atools.sml"
|
neuper@52065
|
212 |
ML_file "Knowledge/simplify.sml"
|
neuper@52065
|
213 |
ML_file "Knowledge/poly.sml"
|
wneuper@59370
|
214 |
ML_file "Knowledge/gcd_poly_ml.sml"
|
wneuper@59370
|
215 |
ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
|
wneuper@59370
|
216 |
ML_file "Knowledge/rational.sml"
|
wneuper@59370
|
217 |
ML_file "Knowledge/equation.sml"
|
wneuper@59370
|
218 |
ML_file "Knowledge/root.sml"
|
wneuper@59370
|
219 |
ML_file "Knowledge/lineq.sml"
|
wneuper@59370
|
220 |
(*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
|
walther@59617
|
221 |
ML_file "Knowledge/rateq.sml" (*exception Size raised "./basis/LibrarySupport.sml")*)
|
wneuper@59370
|
222 |
ML_file "Knowledge/rootrat.sml"
|
wneuper@59370
|
223 |
ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
|
wneuper@59530
|
224 |
ML_file "Knowledge/partial_fractions.sml"
|
walther@59617
|
225 |
(*ML_file "Knowledge/polyeq.sml" exception Size raised "./basis/LibrarySupport.sml")*)
|
neuper@52105
|
226 |
(*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
|
neuper@52065
|
227 |
ML_file "Knowledge/calculus.sml"
|
neuper@52065
|
228 |
ML_file "Knowledge/trig.sml"
|
neuper@52065
|
229 |
(*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
|
neuper@52065
|
230 |
ML_file "Knowledge/diff.sml"
|
neuper@52065
|
231 |
ML_file "Knowledge/integrate.sml"
|
neuper@52065
|
232 |
ML_file "Knowledge/eqsystem.sml"
|
neuper@52065
|
233 |
ML_file "Knowledge/test.sml"
|
neuper@52065
|
234 |
ML_file "Knowledge/polyminus.sml"
|
neuper@52065
|
235 |
ML_file "Knowledge/vect.sml"
|
neuper@52065
|
236 |
ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
|
walther@59617
|
237 |
ML_file "Knowledge/biegelinie-1.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
|
wneuper@59412
|
238 |
(*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
|
walther@59617
|
239 |
ML_file "Knowledge/biegelinie-3.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
|
neuper@52065
|
240 |
ML_file "Knowledge/algein.sml"
|
neuper@52065
|
241 |
ML_file "Knowledge/diophanteq.sml"
|
neuper@52065
|
242 |
ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
|
wneuper@59232
|
243 |
ML_file "Knowledge/inssort.sml"
|
neuper@52065
|
244 |
ML_file "Knowledge/isac.sml"
|
neuper@52065
|
245 |
ML_file "Knowledge/build_thydata.sml"
|
wneuper@59600
|
246 |
|
walther@59617
|
247 |
section \<open>further tests additional to src/.. files\<close>
|
wneuper@59600
|
248 |
ML_file "BridgeLibisabelle/use-cases.sml"
|
wneuper@59144
|
249 |
ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
|
wneuper@59175
|
250 |
ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
|
wneuper@59600
|
251 |
|
wneuper@59472
|
252 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59472
|
253 |
ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59472
|
254 |
ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
|
wneuper@59559
|
255 |
ML \<open>
|
wneuper@59559
|
256 |
\<close> ML \<open>
|
wneuper@59559
|
257 |
\<close> ML \<open>
|
wneuper@59559
|
258 |
\<close>
|
neuper@41943
|
259 |
|
wneuper@59472
|
260 |
section \<open>history of tests\<close>
|
wneuper@59472
|
261 |
text \<open>
|
neuper@48895
|
262 |
Systematic regression tests have been introduced to isac development in 2003.
|
neuper@52139
|
263 |
Sanity of the regression tests suffers from updates following Isabelle development,
|
neuper@48895
|
264 |
which mostly exceeded the resources available in isac's development.
|
neuper@48895
|
265 |
|
neuper@48895
|
266 |
The survey below shall support to efficiently use the tests for isac
|
neuper@48895
|
267 |
on different Isabelle versions. Conclusion in most cases will be:
|
neuper@48895
|
268 |
|
neuper@48895
|
269 |
!!! Use most recent tests or go back to the old notebook
|
neuper@48895
|
270 |
with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
wneuper@59472
|
271 |
\<close>
|
neuper@48895
|
272 |
|
wneuper@59323
|
273 |
|
wneuper@59472
|
274 |
subsection \<open>isac on Isabelle2017\<close>
|
wneuper@59472
|
275 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
276 |
text \<open>
|
wneuper@59449
|
277 |
* Add further signatures, separate structures and cleanup respective files.
|
wneuper@59449
|
278 |
* Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
|
wneuper@59449
|
279 |
* Clean theory dependencies.
|
wneuper@59449
|
280 |
* Start preparing shift from isac-java to Isabelle/jEdit.
|
wneuper@59472
|
281 |
\<close>
|
wneuper@59472
|
282 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59472
|
283 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
284 |
text \<open>
|
wneuper@59449
|
285 |
last changeset with Test_Isac 925fef0f4c81
|
wneuper@59449
|
286 |
first changeset with Test_Isac bbb414976dfe
|
wneuper@59472
|
287 |
\<close>
|
wneuper@59449
|
288 |
|
wneuper@59472
|
289 |
subsection \<open>isac on Isabelle2015\<close>
|
wneuper@59472
|
290 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
291 |
text \<open>
|
wneuper@59373
|
292 |
* Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
|
wneuper@59323
|
293 |
This complicates Test_Isac, see "Prepare running tests" above.
|
wneuper@59323
|
294 |
* Remove TTY interface.
|
wneuper@59323
|
295 |
* Re-activate insertion sort.
|
wneuper@59472
|
296 |
\<close>
|
wneuper@59472
|
297 |
subsubsection \<open>State of tests: unchanged\<close>
|
wneuper@59472
|
298 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
299 |
text \<open>
|
wneuper@59323
|
300 |
last changeset with Test_Isac 2f1b2854927a
|
wneuper@59323
|
301 |
first changeset with Test_Isac ???
|
wneuper@59472
|
302 |
\<close>
|
wneuper@59323
|
303 |
|
wneuper@59472
|
304 |
subsection \<open>isac on Isabelle2014\<close>
|
wneuper@59472
|
305 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
306 |
text \<open>
|
wneuper@59120
|
307 |
migration from "isabelle tty" --> libisabelle
|
wneuper@59472
|
308 |
\<close>
|
wneuper@59120
|
309 |
|
wneuper@59472
|
310 |
subsection \<open>isac on Isabelle2013-2\<close>
|
wneuper@59472
|
311 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
312 |
text \<open>
|
wneuper@55500
|
313 |
reactivated context_thy
|
wneuper@59472
|
314 |
\<close>
|
wneuper@59472
|
315 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
316 |
text \<open>
|
neuper@55319
|
317 |
TODO
|
wneuper@59472
|
318 |
\<close>
|
wneuper@59472
|
319 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
320 |
text \<open>
|
neuper@55319
|
321 |
TODO
|
neuper@55319
|
322 |
:
|
neuper@55319
|
323 |
: isac on Isablle2013-2
|
neuper@55319
|
324 |
:
|
neuper@55319
|
325 |
Changeset: 55318 (03826ceb24da) merged
|
neuper@55319
|
326 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@55319
|
327 |
Date: 2013-12-12 14:27:37 +0100 (7 minutes)
|
wneuper@59472
|
328 |
\<close>
|
neuper@55319
|
329 |
|
wneuper@59472
|
330 |
subsection \<open>isac on Isabelle2013-1\<close>
|
wneuper@59472
|
331 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
332 |
text \<open>
|
neuper@55284
|
333 |
Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
|
neuper@55284
|
334 |
no significant development steps for ISAC.
|
wneuper@59472
|
335 |
\<close>
|
wneuper@59472
|
336 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
337 |
text \<open>
|
neuper@55284
|
338 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
wneuper@59472
|
339 |
\<close>
|
wneuper@59472
|
340 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
341 |
text \<open>
|
neuper@55284
|
342 |
Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
|
neuper@55284
|
343 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@55284
|
344 |
Date: 2013-12-03 18:13:31 +0100 (8 days)
|
neuper@55284
|
345 |
:
|
neuper@55284
|
346 |
: isac on Isablle2013-1
|
neuper@55284
|
347 |
:
|
neuper@55284
|
348 |
Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
|
neuper@55284
|
349 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@55284
|
350 |
Date: 2013-11-21 18:12:17 +0100 (2 weeks)
|
neuper@55284
|
351 |
|
wneuper@59472
|
352 |
\<close>
|
neuper@55284
|
353 |
|
wneuper@59472
|
354 |
subsection \<open>isac on Isabelle2013\<close>
|
wneuper@59472
|
355 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
356 |
text \<open>
|
neuper@52150
|
357 |
# Oct.13: replaced "axioms" by "axiomatization"
|
neuper@52150
|
358 |
# Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
|
neuper@52106
|
359 |
# Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
|
neuper@52106
|
360 |
simplification of multivariate rationals (without improving the rulesets involved).
|
wneuper@59472
|
361 |
\<close>
|
wneuper@59472
|
362 |
subsubsection \<open>Run tests\<close>
|
wneuper@59472
|
363 |
text \<open>
|
neuper@52150
|
364 |
Is standard now; this subsection will be discontinued under Isabelle2013-1
|
wneuper@59472
|
365 |
\<close>
|
wneuper@59472
|
366 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
367 |
text \<open>
|
neuper@52150
|
368 |
See points in subsection "isac on Isabelle2011", "State of tests".
|
neuper@52150
|
369 |
# re-activated listC.sml
|
wneuper@59472
|
370 |
\<close>
|
wneuper@59472
|
371 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
372 |
text \<open>
|
neuper@52175
|
373 |
changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
|
neuper@52175
|
374 |
User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
|
neuper@52175
|
375 |
Date: Tue Nov 19 22:23:30 2013 +0000
|
neuper@52079
|
376 |
:
|
neuper@52079
|
377 |
: isac on Isablle2013
|
neuper@52079
|
378 |
:
|
neuper@52079
|
379 |
Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
|
neuper@52079
|
380 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@52079
|
381 |
Date: 2013-07-15 08:28:50 +0200 (4 weeks)
|
wneuper@59472
|
382 |
\<close>
|
neuper@48895
|
383 |
|
wneuper@59472
|
384 |
subsection \<open>isac on Isabelle2012\<close>
|
wneuper@59472
|
385 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
386 |
text \<open>
|
neuper@48895
|
387 |
isac on Isabelle2012 is considered just a transitional stage
|
neuper@48895
|
388 |
within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
|
neuper@48895
|
389 |
For considerations on the transition see
|
neuper@48895
|
390 |
~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
|
wneuper@59472
|
391 |
\<close>
|
wneuper@59472
|
392 |
subsubsection \<open>Run tests\<close>
|
wneuper@59472
|
393 |
text \<open>
|
neuper@48895
|
394 |
$ cd /usr/local/isabisac12/
|
neuper@48895
|
395 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
396 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59472
|
397 |
\<close>
|
wneuper@59472
|
398 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
399 |
text \<open>
|
neuper@48895
|
400 |
At least the tests from isac on Isabelle2011 run again.
|
neuper@48895
|
401 |
However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
|
neuper@48895
|
402 |
in parallel with evaluation.
|
neuper@48895
|
403 |
|
neuper@48895
|
404 |
Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
|
neuper@48895
|
405 |
yields 69 hits, some of which were already present before Isabelle2002-->2009-2
|
neuper@48895
|
406 |
(i.e. on the old notebook from 2002).
|
neuper@48895
|
407 |
|
neuper@48895
|
408 |
Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
|
neuper@48895
|
409 |
# === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
|
neuper@48895
|
410 |
# === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
|
neuper@48895
|
411 |
# === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
|
neuper@48895
|
412 |
Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
|
neuper@48895
|
413 |
|
neuper@48895
|
414 |
Some tests have been re-activated (e.g. error patterns, fill patterns).
|
wneuper@59472
|
415 |
\<close>
|
wneuper@59472
|
416 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
417 |
text \<open>
|
neuper@52079
|
418 |
Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
|
neuper@52079
|
419 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@52079
|
420 |
Date: 2013-07-11 16:58:31 +0200 (4 weeks)
|
neuper@48895
|
421 |
:
|
neuper@48895
|
422 |
: isac on Isablle2012
|
neuper@48895
|
423 |
:
|
neuper@48895
|
424 |
Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
|
neuper@48895
|
425 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
426 |
Date: 2012-09-24 18:35:13 +0200 (8 months)
|
neuper@48895
|
427 |
------------------------------------------------------------------------------
|
neuper@48895
|
428 |
Changeset: 48756 (7443906996a8) merged
|
neuper@48895
|
429 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
430 |
Date: 2012-09-24 18:15:49 +0200 (8 months)
|
wneuper@59472
|
431 |
\<close>
|
neuper@48895
|
432 |
|
wneuper@59472
|
433 |
subsection \<open>isac on Isabelle2011\<close>
|
wneuper@59472
|
434 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
435 |
text \<open>
|
neuper@48895
|
436 |
isac's mathematics engine has been extended by two developments:
|
neuper@48895
|
437 |
(1) Isabelle's contexts were introduced by Mathias Lehnfeld
|
neuper@52150
|
438 |
(2) Z_Transform was introduced by Jan Rocnik, which revealed
|
neuper@52150
|
439 |
further errors introduced by (1).
|
neuper@52150
|
440 |
(3) "error patterns" were introduced by Gabriella Daroczy
|
neuper@52150
|
441 |
Regressions tests have been added for all of these.
|
wneuper@59472
|
442 |
\<close>
|
wneuper@59472
|
443 |
subsubsection \<open>Run tests\<close>
|
wneuper@59472
|
444 |
text \<open>
|
neuper@48895
|
445 |
$ cd /usr/local/isabisac11/
|
neuper@48895
|
446 |
$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
447 |
$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
|
wneuper@59472
|
448 |
\<close>
|
wneuper@59472
|
449 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
450 |
text \<open>
|
neuper@48895
|
451 |
Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
|
neuper@48895
|
452 |
and sometimes give reasons for failing tests.
|
neuper@48895
|
453 |
(*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
|
neuper@48895
|
454 |
work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
|
neuper@48895
|
455 |
|
neuper@48895
|
456 |
The most signification tests (in particular Frontend/interface.sml) run,
|
neuper@48895
|
457 |
however, many "error in kernel" are not caught by an exception.
|
neuper@48895
|
458 |
------------------------------------------------------------------------------
|
neuper@48895
|
459 |
After the changeset below Test_Isac worked with check_unsynchronized_ref ():
|
neuper@48895
|
460 |
------------------------------------------------------------------------------
|
neuper@48895
|
461 |
Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
|
neuper@48895
|
462 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
463 |
Date: 2012-08-06 10:38:11 +0200 (11 months)
|
neuper@52150
|
464 |
|
neuper@52150
|
465 |
|
neuper@52150
|
466 |
The list below records TODOs while producing an ISAC kernel for
|
neuper@52150
|
467 |
gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
|
neuper@52150
|
468 |
(so to be resumed with Isabelle2013-1):
|
neuper@52150
|
469 |
############## WNxxxxxx.TODO can be found in sources ##############
|
neuper@52150
|
470 |
--------------------------------------------------------------------------------
|
neuper@52150
|
471 |
WN111013.TODO: lots of cleanup/removal in test/../Test.thy
|
neuper@52150
|
472 |
--------------------------------------------------------------------------------
|
neuper@52150
|
473 |
WN111013.TODO: remove concept around "fun init_form", lots of troubles with
|
neuper@52150
|
474 |
this special case (see) --- why not nxt = Model_Problem here ? ---
|
neuper@52150
|
475 |
--------------------------------------------------------------------------------
|
neuper@52150
|
476 |
WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
|
neuper@52150
|
477 |
... FIRST redesign
|
neuper@52150
|
478 |
# simplify_* , *_simp_*
|
neuper@52150
|
479 |
# norm_*
|
neuper@52150
|
480 |
# calc_* , calculate_* ... require iteration over all rls ...
|
neuper@52150
|
481 |
... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
|
neuper@52150
|
482 |
--------------------------------------------------------------------------------
|
neuper@52150
|
483 |
WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
|
neuper@52150
|
484 |
--------------------------------------------------------------------------------
|
neuper@52150
|
485 |
WN120314 changeset a393bb9f5e9f drops root equations.
|
neuper@52150
|
486 |
see test/Tools/isac/Knowledge/rootrateq.sml
|
neuper@52150
|
487 |
--------------------------------------------------------------------------------
|
neuper@52150
|
488 |
WN120317.TODO changeset 977788dfed26 dropped rateq:
|
neuper@52150
|
489 |
# test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
|
neuper@52150
|
490 |
# test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
|
neuper@52150
|
491 |
investigation Check_elementwise stopped due to too much effort finding out,
|
neuper@52150
|
492 |
why Check_elementwise worked in 2002 in spite of the error.
|
neuper@52150
|
493 |
--------------------------------------------------------------------------------
|
neuper@52150
|
494 |
WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
|
neuper@52150
|
495 |
--------------------------------------------------------------------------------
|
neuper@52150
|
496 |
WN120317.TODO found by test --- interSteps for Schalk 299a --- that
|
neuper@52150
|
497 |
NO test with 'interSteps' is checked properly (with exn on changed behaviour)
|
neuper@52150
|
498 |
--------------------------------------------------------------------------------
|
neuper@52150
|
499 |
WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
|
neuper@52150
|
500 |
a newly outcommented test where rewrite_set_ make_polynomial --> NONE
|
neuper@52150
|
501 |
--------------------------------------------------------------------------------
|
neuper@52150
|
502 |
WN120320.TODO check-improve rlsthmsNOTisac:
|
neuper@52150
|
503 |
DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
|
neuper@52150
|
504 |
DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
|
neuper@52150
|
505 |
FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
|
neuper@52150
|
506 |
# mark twice thms (in isac + (later) in Isabelle) in Isac.thy
|
neuper@52150
|
507 |
--------------------------------------------------------------------------------
|
neuper@52150
|
508 |
WN120320.TODO rlsthmsNOTisac: replace twice thms ^
|
neuper@52150
|
509 |
--------------------------------------------------------------------------------
|
neuper@52150
|
510 |
WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
|
neuper@52150
|
511 |
--- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
|
neuper@52150
|
512 |
--------------------------------------------------------------------------------
|
neuper@52150
|
513 |
WN120321.TODO rearrange theories:
|
neuper@52150
|
514 |
Knowledge
|
neuper@52150
|
515 |
:
|
walther@59603
|
516 |
Prog_Expr.thy
|
neuper@52150
|
517 |
///Descript.thy --> ProgLang
|
walther@59603
|
518 |
Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
|
neuper@52150
|
519 |
ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
|
neuper@52150
|
520 |
Interpret.thy are generated (simplifies xml structure for theories)
|
wneuper@59585
|
521 |
Program.thy
|
neuper@52150
|
522 |
Tools.thy
|
neuper@52150
|
523 |
ListC.thy <--- first_Proglang_thy
|
neuper@52150
|
524 |
--------------------------------------------------------------------------------
|
neuper@52150
|
525 |
WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
|
neuper@52150
|
526 |
EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
|
neuper@52150
|
527 |
broken during work on thy-hierarchy
|
neuper@52150
|
528 |
--------------------------------------------------------------------------------
|
neuper@52150
|
529 |
WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
|
neuper@55421
|
530 |
test --- the_hier (get_thes ()) (collect_thydata ())---
|
neuper@52150
|
531 |
--------------------------------------------------------------------------------
|
neuper@52150
|
532 |
WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
|
neuper@52150
|
533 |
!!add mutual crossreferences to ?fun headline??? where the same has to be done:
|
neuper@52150
|
534 |
!!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
|
neuper@52150
|
535 |
--------------------------------------------------------------------------------
|
neuper@52150
|
536 |
WN120409.TODO replace "op mem" (2002) with member (2011) ...
|
neuper@52150
|
537 |
... an exercise interesting for beginners !
|
neuper@52150
|
538 |
--------------------------------------------------------------------------------
|
neuper@52150
|
539 |
WN120411 scanning html representation of newly generated knowledge:
|
neuper@52150
|
540 |
* thy:
|
neuper@52150
|
541 |
** Theorems: only "Proof of the theorem" (correct!)
|
neuper@52150
|
542 |
and "(c) isac-team (math-autor)"
|
neuper@52150
|
543 |
** Rulesets: only "Identifier:///"
|
neuper@52150
|
544 |
and "(c) isac-team (math-autor)"
|
neuper@52150
|
545 |
** IsacKnowledge: link to dependency graph (which needs to be created first)
|
neuper@52150
|
546 |
** IsacScripts --> ProgramLanguage
|
neuper@52150
|
547 |
*** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
|
neuper@52150
|
548 |
|
neuper@52150
|
549 |
* pbl: OK !?!
|
neuper@52150
|
550 |
* met: OK !?!
|
neuper@52150
|
551 |
* exp:
|
neuper@52150
|
552 |
** Z-Transform is missing !!!
|
neuper@52150
|
553 |
** type-constraints !!!
|
neuper@52150
|
554 |
--------------------------------------------------------------------------------
|
neuper@52150
|
555 |
WN120417: merging xmldata revealed:
|
neuper@52150
|
556 |
..............NEWLY generated:........................................
|
neuper@52150
|
557 |
<THEOREMDATA>
|
neuper@52150
|
558 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
neuper@52150
|
559 |
<STRINGLIST>
|
neuper@52150
|
560 |
<STRING> Isabelle </STRING>
|
neuper@52150
|
561 |
<STRING> Fun </STRING>
|
neuper@52150
|
562 |
<STRING> Theorems </STRING>
|
neuper@52150
|
563 |
<STRING> o_apply </STRING>
|
neuper@52150
|
564 |
</STRINGLIST>
|
neuper@52150
|
565 |
<MATHML>
|
neuper@52150
|
566 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
neuper@52150
|
567 |
</MATHML> <PROOF>
|
neuper@52150
|
568 |
<EXTREF>
|
neuper@52150
|
569 |
<TEXT> Proof of the theorem </TEXT>
|
neuper@52150
|
570 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
neuper@52150
|
571 |
</EXTREF>
|
neuper@52150
|
572 |
</PROOF>
|
neuper@52150
|
573 |
<EXPLANATIONS> </EXPLANATIONS>
|
neuper@52150
|
574 |
<MATHAUTHORS>
|
neuper@52150
|
575 |
<STRING> Isabelle team, TU Munich </STRING>
|
neuper@52150
|
576 |
</MATHAUTHORS>
|
neuper@52150
|
577 |
<COURSEDESIGNS>
|
neuper@52150
|
578 |
</COURSEDESIGNS>
|
neuper@52150
|
579 |
</THEOREMDATA>
|
neuper@52150
|
580 |
..............OLD FORMAT:.............................................
|
neuper@52150
|
581 |
<THEOREMDATA>
|
neuper@52150
|
582 |
<GUH> thy_isab_Fun-thm-o_apply </GUH>
|
neuper@52150
|
583 |
<STRINGLIST>
|
neuper@52150
|
584 |
<STRING> Isabelle </STRING>
|
neuper@52150
|
585 |
<STRING> Fun </STRING>
|
neuper@52150
|
586 |
<STRING> Theorems </STRING>
|
neuper@52150
|
587 |
<STRING> o_apply </STRING>
|
neuper@52150
|
588 |
</STRINGLIST>
|
neuper@52150
|
589 |
<THEOREM>
|
neuper@52150
|
590 |
<ID> o_apply </ID>
|
neuper@52150
|
591 |
<MATHML>
|
neuper@52150
|
592 |
<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
|
neuper@52150
|
593 |
</MATHML>
|
neuper@52150
|
594 |
</THEOREM>
|
neuper@52150
|
595 |
<PROOF>
|
neuper@52150
|
596 |
<EXTREF>
|
neuper@52150
|
597 |
<TEXT> Proof of the theorem </TEXT>
|
neuper@52150
|
598 |
<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
|
neuper@52150
|
599 |
</EXTREF>
|
neuper@52150
|
600 |
</PROOF>
|
neuper@52150
|
601 |
<EXPLANATIONS> </EXPLANATIONS>
|
neuper@52150
|
602 |
<MATHAUTHORS>
|
neuper@52150
|
603 |
<STRING> Isabelle team, TU Munich </STRING>
|
neuper@52150
|
604 |
</MATHAUTHORS>
|
neuper@52150
|
605 |
<COURSEDESIGNS>
|
neuper@52150
|
606 |
</COURSEDESIGNS>
|
neuper@52150
|
607 |
</THEOREMDATA>
|
neuper@52150
|
608 |
--------------------------------------------------------------------------------
|
wneuper@59472
|
609 |
\<close>
|
wneuper@59472
|
610 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
611 |
text \<open>
|
neuper@48895
|
612 |
isac development was done between these changesets:
|
neuper@48895
|
613 |
------------------------------------------------------------------------------
|
neuper@48895
|
614 |
Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
|
neuper@48895
|
615 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
616 |
Date: 2012-09-24 16:39:30 +0200 (8 months)
|
neuper@48895
|
617 |
:
|
neuper@48895
|
618 |
: isac on Isablle2011
|
neuper@48895
|
619 |
:
|
neuper@48895
|
620 |
Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
|
neuper@48895
|
621 |
Branch: decompose-isar
|
neuper@48895
|
622 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
623 |
Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
|
neuper@48895
|
624 |
------------------------------------------------------------------------------
|
wneuper@59472
|
625 |
\<close>
|
neuper@48895
|
626 |
|
wneuper@59472
|
627 |
subsection \<open>isac on Isabelle2009-2\<close>
|
wneuper@59472
|
628 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
629 |
text \<open>
|
neuper@48895
|
630 |
In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
|
neuper@48895
|
631 |
The update was painful (bridging 7 years of Isabelle development) and cut short
|
neuper@48895
|
632 |
due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
|
neuper@48895
|
633 |
going on to Isabelle2011 although most of the tests did not run.
|
wneuper@59472
|
634 |
\<close>
|
wneuper@59472
|
635 |
subsubsection \<open>Run tests\<close>
|
wneuper@59472
|
636 |
text \<open>
|
neuper@52150
|
637 |
WN131021 this is broken by installation of Isabelle2011/12/13,
|
neuper@52150
|
638 |
because all these write their binaries to ~/.isabelle/heaps/..
|
neuper@52150
|
639 |
|
neuper@48895
|
640 |
$ cd /usr/local/isabisac09-2/
|
neuper@48895
|
641 |
$ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
|
neuper@48895
|
642 |
$ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
|
neuper@48895
|
643 |
NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
|
wneuper@59472
|
644 |
\<close>
|
wneuper@59472
|
645 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
646 |
text \<open>
|
neuper@48895
|
647 |
Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
|
wneuper@59472
|
648 |
\<close>
|
wneuper@59472
|
649 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
650 |
text \<open>
|
neuper@48895
|
651 |
isac development was done between these changesets:
|
neuper@48895
|
652 |
------------------------------------------------------------------------------
|
neuper@48895
|
653 |
Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
|
neuper@48895
|
654 |
Branch: decompose-isar
|
neuper@48895
|
655 |
User: Marco Steger <m.steger@student.tugraz.at>
|
neuper@48895
|
656 |
Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
|
neuper@48895
|
657 |
:
|
neuper@48895
|
658 |
: isac on Isablle2009-2
|
neuper@48895
|
659 |
:
|
neuper@48895
|
660 |
Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
|
neuper@48895
|
661 |
Branch: isac-from-Isabelle2009-2
|
neuper@48895
|
662 |
User: Walther Neuper <neuper@ist.tugraz.at>
|
neuper@48895
|
663 |
Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
|
neuper@48895
|
664 |
------------------------------------------------------------------------------
|
wneuper@59472
|
665 |
\<close>
|
neuper@48895
|
666 |
|
wneuper@59472
|
667 |
subsection \<open>isac on Isabelle2002\<close>
|
wneuper@59472
|
668 |
subsubsection \<open>Summary of development\<close>
|
wneuper@59472
|
669 |
text \<open>
|
neuper@48895
|
670 |
From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
|
neuper@48895
|
671 |
of isac's mathematics engine has been implemented.
|
wneuper@59472
|
672 |
\<close>
|
wneuper@59472
|
673 |
subsubsection \<open>Run tests\<close>
|
wneuper@59472
|
674 |
subsubsection \<open>State of tests\<close>
|
wneuper@59472
|
675 |
text \<open>
|
neuper@48895
|
676 |
All tests work on an old notebook (the right PolyML coudn't be upgraded to more
|
neuper@48895
|
677 |
recent Linux versions)
|
wneuper@59472
|
678 |
\<close>
|
wneuper@59472
|
679 |
subsubsection \<open>Changesets of begin and end\<close>
|
wneuper@59472
|
680 |
text \<open>
|
neuper@48895
|
681 |
Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
|
neuper@48895
|
682 |
see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
|
wneuper@59472
|
683 |
\<close>
|
neuper@48895
|
684 |
|
neuper@41943
|
685 |
end
|
neuper@52065
|
686 |
(*========== inhibit exn 130719 Isabelle2013 ===================================
|
neuper@52065
|
687 |
============ inhibit exn 130719 Isabelle2013 =================================*)
|
neuper@41943
|
688 |
|
neuper@41943
|
689 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
|
neuper@48895
|
690 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
|
neuper@41975
|
691 |
|