neuper@38009
|
1 |
(* Title Run_Tests on isac
|
neuper@37985
|
2 |
$ cd /usr/local/isabisac/test/Tools/isac
|
neuper@38010
|
3 |
$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
|
neuper@37985
|
4 |
|
neuper@38024
|
5 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@38024
|
6 |
!!!!!!! actual version is src/Tools/isac/Test_isac.thy !!!!!!!
|
neuper@38024
|
7 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@38024
|
8 |
|
neuper@38010
|
9 |
RESTART emacs after having created a new Isac heap.
|
neuper@38009
|
10 |
was sml/RTEST-root.sml in isac-2002
|
neuper@38011
|
11 |
|
neuper@38011
|
12 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890
|
neuper@38011
|
13 |
10 20 30 40 50 60 70 80
|
neuper@37985
|
14 |
*)
|
neuper@37985
|
15 |
|
neuper@38009
|
16 |
theory Test_Isac imports Isac begin
|
neuper@38022
|
17 |
|
neuper@38009
|
18 |
ML{* writeln "**** run the tests **************************************" *};
|
neuper@38010
|
19 |
ML {* Toplevel.debug := true; *}
|
neuper@38009
|
20 |
(*
|
neuper@38009
|
21 |
cd "systest";
|
neuper@38009
|
22 |
(*+ check kbtest/diffapp.sml for additional items in met-model*)
|
neuper@38009
|
23 |
use"root-equ.sml";
|
neuper@38009
|
24 |
use"script.sml";
|
neuper@38009
|
25 |
(* use"script_if.sml"; WN03 missing: is_rootequation_in*)
|
neuper@38009
|
26 |
use"scriptnew.sml";
|
neuper@38009
|
27 |
use"subp-rooteq.sml";
|
neuper@38009
|
28 |
use"tacis.sml";
|
neuper@38009
|
29 |
use"interface-xml.sml";
|
neuper@38009
|
30 |
(* use"testdaten.sml"; no update after dropping 'errorBound'*)
|
neuper@38009
|
31 |
cd "../..";
|
neuper@38009
|
32 |
*)
|
neuper@38009
|
33 |
ML{* writeln "**** run systests complete ******************************" *};
|
neuper@38022
|
34 |
|
neuper@38022
|
35 |
ML {*
|
neuper@38022
|
36 |
val t1 = @{term "1+2::real"};
|
neuper@38022
|
37 |
val t2 = @{term "abc"};
|
neuper@38022
|
38 |
term2str t2 = "abc";
|
neuper@38022
|
39 |
fun terms2str ts = (strs2str o (map term2str )) ts;
|
neuper@38022
|
40 |
terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";
|
neuper@38022
|
41 |
fun terms2str' ts = (strs2str' o (map term2str )) ts;
|
neuper@38022
|
42 |
terms2str' [t1,t2] = "[1 + 2,abc]";
|
neuper@38022
|
43 |
fun terms2strs ts = (map term2str) ts;
|
neuper@38022
|
44 |
terms2strs [t1,t2] = ["1 + 2", "abc"];
|
neuper@38022
|
45 |
*}
|
neuper@38022
|
46 |
|
neuper@38009
|
47 |
(*
|
neuper@38009
|
48 |
cd"smltest/Scripts";
|
neuper@38009
|
49 |
use"calculate-float.sml";
|
neuper@38022
|
50 |
*)
|
neuper@38022
|
51 |
use"ProgLang/calculate.sml"; (*part.*)
|
neuper@38022
|
52 |
(*
|
neuper@38009
|
53 |
use"listg.sml";
|
neuper@38022
|
54 |
*)
|
neuper@38022
|
55 |
use"ProgLang/rewrite.sml"; (*part.*)
|
neuper@38022
|
56 |
(*
|
neuper@38009
|
57 |
use"scrtools.sml";
|
neuper@38025
|
58 |
use"termC.sml";
|
neuper@38009
|
59 |
use"tools.sml";
|
neuper@38009
|
60 |
cd "../..";
|
neuper@38009
|
61 |
cd"smltest/ME";
|
neuper@38009
|
62 |
use"ctree.sml";
|
neuper@38009
|
63 |
*)
|
neuper@38011
|
64 |
use "Interpret/calchead.sml" (*part.*)
|
neuper@38009
|
65 |
(*
|
neuper@38009
|
66 |
use"calchead.sml";
|
neuper@38009
|
67 |
use"rewtools.sml";
|
neuper@38009
|
68 |
use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
|
neuper@38009
|
69 |
use"inform.sml";
|
neuper@38009
|
70 |
use"me.sml";
|
neuper@38009
|
71 |
use"ptyps.sml";
|
neuper@38009
|
72 |
cd "../..";
|
neuper@38009
|
73 |
cd"smltest/xmlsrc";
|
neuper@38009
|
74 |
use"datatypes.sml";
|
neuper@38009
|
75 |
use"pbl-met-hierarchy.sml";
|
neuper@38009
|
76 |
use"thy-hierarchy.sml";
|
neuper@38009
|
77 |
cd "../..";
|
neuper@38009
|
78 |
cd"smltest/FE-interface";
|
neuper@38009
|
79 |
use"interface.sml";
|
neuper@38009
|
80 |
cd "../..";
|
neuper@38009
|
81 |
*)
|
neuper@38009
|
82 |
ML{* writeln "**** run tests on math-engine complete ******************" *};
|
neuper@38009
|
83 |
(*
|
neuper@38009
|
84 |
cd"smltest/IsacKnowledge";
|
neuper@38009
|
85 |
use"atools.sml";
|
neuper@38009
|
86 |
use"complex.sml";
|
neuper@38009
|
87 |
use"diff.sml";
|
neuper@38009
|
88 |
use"diffapp.sml";
|
neuper@38022
|
89 |
(**)
|
neuper@38022
|
90 |
use "Knowledge/integrate.sml"; (*part.*)
|
neuper@38013
|
91 |
|
neuper@38009
|
92 |
use"equation.sml";
|
neuper@38009
|
93 |
(*use"inssort.sml"; problems with recdef in Isabelle2002*)
|
neuper@38009
|
94 |
use"logexp.sml";
|
neuper@38022
|
95 |
*)
|
neuper@38022
|
96 |
use"Knowledge/poly.sml"; (*part.*)
|
neuper@38022
|
97 |
(*
|
neuper@38009
|
98 |
use"polyminus.sml";
|
neuper@38009
|
99 |
use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
|
neuper@38009
|
100 |
? also check others without check 'diff.behav.'*);
|
neuper@38009
|
101 |
use"rateq.sml";
|
neuper@38009
|
102 |
use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
|
neuper@38009
|
103 |
use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
|
neuper@38009
|
104 |
for simplification search MG
|
neuper@38009
|
105 |
erls: 98a(1) 104a(1) 104a(2) 68a *);
|
neuper@38009
|
106 |
use"root.sml";
|
neuper@38009
|
107 |
use"rooteq.sml";
|
neuper@38009
|
108 |
use"rootrateq.sml";
|
neuper@38009
|
109 |
use"termorder.sml";
|
neuper@38009
|
110 |
use"trig.sml";
|
neuper@38009
|
111 |
use"vect.sml";
|
neuper@38009
|
112 |
use"wn.sml";
|
neuper@38009
|
113 |
use"eqsystem.sml";
|
neuper@38009
|
114 |
use"biegelinie.sml";
|
neuper@38009
|
115 |
use"algein.sml";
|
neuper@38009
|
116 |
cd "../..";
|
neuper@38009
|
117 |
*)
|
neuper@38022
|
118 |
(* TODO
|
neuper@38022
|
119 |
use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
|
neuper@38022
|
120 |
|
neuper@38022
|
121 |
*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
|
neuper@38022
|
122 |
*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
|
neuper@38022
|
123 |
|
neuper@38022
|
124 |
use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
|
neuper@38022
|
125 |
*)
|
neuper@38013
|
126 |
use_thy "../../Pure/Isar/Test_Parse_Term"
|
neuper@38013
|
127 |
use_thy "../../Pure/Isar/Test_Parsers"
|
neuper@38013
|
128 |
|
neuper@38009
|
129 |
ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
|
neuper@38009
|
130 |
(*
|
neuper@38009
|
131 |
val path = "/home/neuper/proto2/testsml2xml/";
|
neuper@38009
|
132 |
pbl_hierarchy2file (path ^ "pbl/");
|
neuper@38009
|
133 |
pbls2file (path ^ "pbl/");
|
neuper@38009
|
134 |
met_hierarchy2file (path ^ "met/");
|
neuper@38009
|
135 |
mets2file (path ^ "met/");
|
neuper@38009
|
136 |
thy_hierarchy2file (path ^ "thy/");
|
neuper@38009
|
137 |
thes2file (path ^ "thy/");
|
neuper@38009
|
138 |
cd"sml";
|
neuper@38009
|
139 |
*)
|
neuper@38009
|
140 |
ML{* writeln "**** tested creation of xmldata *************************" *};
|
neuper@37985
|
141 |
|
neuper@38009
|
142 |
ML{*states:=[];
|
neuper@38009
|
143 |
writeln "=========================================================";
|
neuper@38009
|
144 |
|
neuper@38009
|
145 |
writeln "**** run systests complete ***************** re-organize!";
|
neuper@38009
|
146 |
writeln "**** run tests on math-engine complete ******************";
|
neuper@38009
|
147 |
writeln "**** run tests on IsacKnowledge complete ****************";
|
neuper@38009
|
148 |
writeln "**** build isac kernel + run tests complete *************";
|
neuper@38009
|
149 |
writeln "**** tested creation of xmldata *************************";
|
neuper@38009
|
150 |
*}
|
neuper@37985
|
151 |
|
neuper@37985
|
152 |
end
|