author | Walther Neuper <neuper@ist.tugraz.at> |
Mon, 21 Feb 2011 19:40:36 +0100 | |
branch | decompose-isar |
changeset 40836 | 69364e021751 |
parent 38085 | 45de545f1699 |
child 41924 | 7407ceef2aed |
permissions | -rw-r--r-- |
neuper@38051 | 1 |
(* Title: Run_Tests on isac |
neuper@38051 | 2 |
Author: Walther Neuper 100808 |
neuper@38051 | 3 |
(c) due to copyright terms |
neuper@38051 | 4 |
|
neuper@38053 | 5 |
$ cd /usr/local/isabisac/src/Tools/isac |
neuper@38024 | 6 |
$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy & |
neuper@38043 | 7 |
$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy & |
neuper@38024 | 8 |
|
neuper@38053 | 9 |
RESTART emacs after having created a new Isac heap with |
neuper@38053 | 10 |
$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac |
neuper@38024 | 11 |
|
neuper@38024 | 12 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
neuper@38024 | 13 |
10 20 30 40 50 60 70 80 |
neuper@38024 | 14 |
*) |
neuper@38024 | 15 |
|
neuper@38036 | 16 |
theory Test_Isac imports "Knowledge/Isac" begin |
neuper@38024 | 17 |
|
neuper@38024 | 18 |
ML{* writeln "**** run the tests **************************************" *}; |
neuper@38024 | 19 |
ML {* Toplevel.debug := true; *} |
neuper@38024 | 20 |
(* |
neuper@38024 | 21 |
cd "systest"; |
neuper@38024 | 22 |
(*+ check kbtest/diffapp.sml for additional items in met-model*) |
neuper@38024 | 23 |
use"root-equ.sml"; |
neuper@38024 | 24 |
use"script.sml"; |
neuper@38024 | 25 |
(* use"script_if.sml"; WN03 missing: is_rootequation_in*) |
neuper@38024 | 26 |
use"scriptnew.sml"; |
neuper@38024 | 27 |
use"subp-rooteq.sml"; |
neuper@38024 | 28 |
use"tacis.sml"; |
neuper@38024 | 29 |
use"interface-xml.sml"; |
neuper@38024 | 30 |
(* use"testdaten.sml"; no update after dropping 'errorBound'*) |
neuper@38024 | 31 |
cd "../.."; |
neuper@38024 | 32 |
*) |
neuper@38024 | 33 |
ML{* writeln "**** run systests complete ******************************" *}; |
neuper@38061 | 34 |
|
neuper@38061 | 35 |
use"../../../test/Tools/isac/calcelems.sml"; (*complete*) |
neuper@38061 | 36 |
|
neuper@38024 | 37 |
(* |
neuper@38024 | 38 |
cd"smltest/Scripts"; |
neuper@38024 | 39 |
*) |
neuper@38025 | 40 |
use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*) |
neuper@38051 | 41 |
|
neuper@38051 | 42 |
|
neuper@38025 | 43 |
use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*) |
neuper@38036 | 44 |
use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*) |
neuper@38024 | 45 |
(* |
neuper@38024 | 46 |
use"listg.sml"; |
neuper@38024 | 47 |
use"scrtools.sml"; |
neuper@38024 | 48 |
use"tools.sml"; |
neuper@38024 | 49 |
cd "../.."; |
neuper@38024 | 50 |
cd"smltest/ME"; |
neuper@38024 | 51 |
*) |
neuper@38036 | 52 |
use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*) |
neuper@38036 | 53 |
(* use"ctree.sml"; |
neuper@38036 | 54 |
*) |
neuper@38036 | 55 |
use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*) |
neuper@38051 | 56 |
use "../../../test/Tools/isac/Interpret/calchead.sml"; |
neuper@38061 | 57 |
ML {*print_depth 999*} |
neuper@38061 | 58 |
use "../../../test/Tools/isac/Interpret/rewtools.sml"; (**) |
neuper@38024 | 59 |
(* |
neuper@38024 | 60 |
use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
neuper@38024 | 61 |
use"inform.sml"; |
neuper@38065 | 62 |
*) |
neuper@38065 | 63 |
ML {*print_depth 5*} |
neuper@38065 | 64 |
use "../../../test/Tools/isac/Interpret/mathengine.sml"; (*part.*) |
neuper@38065 | 65 |
(* |
neuper@38024 | 66 |
use"me.sml"; |
neuper@38024 | 67 |
cd "../.."; |
neuper@38024 | 68 |
cd"smltest/xmlsrc"; |
neuper@38024 | 69 |
use"datatypes.sml"; |
neuper@38024 | 70 |
use"pbl-met-hierarchy.sml"; |
neuper@38061 | 71 |
use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"; (**) |
neuper@38056 | 72 |
*) |
neuper@38061 | 73 |
|
neuper@38056 | 74 |
use"../../../test/Tools/isac/Frontend/interface.sml"; (**) |
neuper@38056 | 75 |
(* |
neuper@38024 | 76 |
cd "../.."; |
neuper@38024 | 77 |
*) |
neuper@38024 | 78 |
ML{* writeln "**** run tests on math-engine complete ******************" *}; |
neuper@38024 | 79 |
(* |
neuper@38081 | 80 |
cd"smltest/IsacKnowledge"; ---below the order as in theory Isac--- |
neuper@38024 | 81 |
use"atools.sml"; |
neuper@38036 | 82 |
use"termorder.sml"; |
neuper@38036 | 83 |
*) |
neuper@38065 | 84 |
ML {* |
neuper@38065 | 85 |
print_depth 999 |
neuper@38065 | 86 |
*} |
neuper@38066 | 87 |
ML {*print_depth 5*} |
neuper@38065 | 88 |
use"../../../test/Tools/isac/Knowledge/simplify.sml"; (*part.*) |
neuper@38065 | 89 |
(* |
neuper@38065 | 90 |
use"poly.sml" |
neuper@38065 | 91 |
*) |
neuper@38048 | 92 |
use"../../../test/Tools/isac/Knowledge/rational.sml"; (*part.*) |
neuper@38036 | 93 |
(* |
neuper@38036 | 94 |
use"equation.sml"; |
neuper@38036 | 95 |
use"root.sml"; |
neuper@38063 | 96 |
*) |
neuper@38063 | 97 |
use "../../../test/Tools/isac/Knowledge/inssort.sml"; (*part.*) |
neuper@38063 | 98 |
(* |
neuper@38036 | 99 |
(*use"inssort.sml"; problems with recdef in Isabelle2002*) |
neuper@38036 | 100 |
use"rooteq.sml"; |
neuper@38036 | 101 |
use"rateq.sml"; |
neuper@38036 | 102 |
use"rootrateq.sml"; |
neuper@38036 | 103 |
|
neuper@38036 | 104 |
use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN |
neuper@38036 | 105 |
? also check others without check 'diff.behav.'*); |
neuper@38036 | 106 |
use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', |
neuper@38036 | 107 |
for simplification search MG |
neuper@38036 | 108 |
erls: 98a(1) 104a(1) 104a(2) 68a *); |
neuper@38036 | 109 |
use"wn.sml"; |
neuper@38036 | 110 |
use"trig.sml"; |
neuper@38036 | 111 |
use"logexp.sml"; |
neuper@38030 | 112 |
*) |
neuper@38065 | 113 |
ML {*print_depth 5*} |
neuper@38082 | 114 |
use "../../../test/Tools/isac/Knowledge/diff.sml"; (* *) |
neuper@38065 | 115 |
use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*complete*) |
neuper@38030 | 116 |
(* |
neuper@38036 | 117 |
use"eqsystem.sml"; |
neuper@38037 | 118 |
*) |
neuper@38085 | 119 |
ML {*print_depth 5*} |
neuper@38057 | 120 |
use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (* part. *) |
neuper@38037 | 121 |
(* |
neuper@38024 | 122 |
use"vect.sml"; |
neuper@38036 | 123 |
use"diffapp.sml"; |
neuper@38024 | 124 |
use"biegelinie.sml"; |
neuper@38024 | 125 |
use"algein.sml"; |
neuper@38057 | 126 |
*) |
neuper@38061 | 127 |
ML {* |
neuper@40836 | 128 |
Thy_Info.get_theory "Isac" |
neuper@38061 | 129 |
*} |
neuper@38057 | 130 |
use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) |
neuper@38080 | 131 |
|
neuper@38061 | 132 |
ML {*print_depth 3*} |
neuper@38057 | 133 |
ML {*111*} |
neuper@38057 | 134 |
|
neuper@38057 | 135 |
(* |
neuper@38024 | 136 |
cd "../.."; |
neuper@38024 | 137 |
*) |
neuper@38024 | 138 |
(* TODO |
neuper@38024 | 139 |
use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test" |
neuper@38057 | 140 |
: |
neuper@38024 | 141 |
*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library" |
neuper@40836 | 142 |
*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language" |
neuper@38024 | 143 |
|
neuper@38024 | 144 |
use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" |
neuper@38080 | 145 |
*) |
neuper@38080 | 146 |
use "../../../test/Pure/library.sml" (**) |
neuper@38061 | 147 |
use_thy "../../../test/Pure/General/Basics" |
neuper@38061 | 148 |
|
neuper@38025 | 149 |
use_thy "../../../test/Pure/Isar/Test_Parse_Term" |
neuper@38025 | 150 |
use_thy "../../../test/Pure/Isar/Test_Parsers" |
neuper@38024 | 151 |
|
neuper@38024 | 152 |
ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; |
neuper@38024 | 153 |
(* |
neuper@38025 | 154 |
val path = "/home/neuper/proto3/testsml2xml/"; |
neuper@38024 | 155 |
pbl_hierarchy2file (path ^ "pbl/"); |
neuper@38024 | 156 |
pbls2file (path ^ "pbl/"); |
neuper@38024 | 157 |
met_hierarchy2file (path ^ "met/"); |
neuper@38024 | 158 |
mets2file (path ^ "met/"); |
neuper@38024 | 159 |
thy_hierarchy2file (path ^ "thy/"); |
neuper@38024 | 160 |
thes2file (path ^ "thy/"); |
neuper@38024 | 161 |
cd"sml"; |
neuper@38024 | 162 |
*) |
neuper@38024 | 163 |
ML{* writeln "**** tested creation of xmldata *************************" *}; |
neuper@38024 | 164 |
|
neuper@38024 | 165 |
ML{*states:=[]; |
neuper@38024 | 166 |
writeln "========================================================="; |
neuper@38024 | 167 |
|
neuper@38024 | 168 |
writeln "**** run systests complete ***************** re-organize!"; |
neuper@38024 | 169 |
writeln "**** run tests on math-engine complete ******************"; |
neuper@38024 | 170 |
writeln "**** run tests on IsacKnowledge complete ****************"; |
neuper@38024 | 171 |
writeln "**** build isac kernel + run tests complete *************"; |
neuper@38024 | 172 |
writeln "**** tested creation of xmldata *************************"; |
neuper@38024 | 173 |
*} |
neuper@38024 | 174 |
|
neuper@38024 | 175 |
end |
neuper@38051 | 176 |
|
neuper@38051 | 177 |
(*=== inhibit exn ?============================================================= |
neuper@38051 | 178 |
===== inhibit exn ?===========================================================*) |
neuper@38051 | 179 |
|
neuper@38056 | 180 |
|
neuper@38051 | 181 |
(*========== inhibit exn ======================================================= |
neuper@38056 | 182 |
|
neuper@38056 | 183 |
"########### testcode inserted vvv ###########################################"; |
neuper@38056 | 184 |
"########### testcode inserted ^^^ ###########################################"; |
neuper@38056 | 185 |
|
neuper@38051 | 186 |
============ inhibit exn =====================================================*) |
neuper@38051 | 187 |
|
neuper@38056 | 188 |
|
neuper@38051 | 189 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
neuper@38051 | 190 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |