author | Walther Neuper <neuper@ist.tugraz.at> |
Tue, 14 Sep 2010 15:46:56 +0200 | |
branch | isac-update-Isa09-2 |
changeset 38010 | a37a3ab989f4 |
parent 38009 | b49723351533 |
child 38011 | 3147f2c1525c |
permissions | -rw-r--r-- |
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@38010 | 5 |
RESTART emacs after having created a new Isac heap. |
neuper@38009 | 6 |
was sml/RTEST-root.sml in isac-2002 |
neuper@37985 | 7 |
*) |
neuper@37985 | 8 |
|
neuper@38009 | 9 |
theory Test_Isac imports Isac begin |
neuper@38009 | 10 |
|
neuper@38009 | 11 |
ML{* writeln "**** run the tests **************************************" *}; |
neuper@38010 | 12 |
ML {* Toplevel.debug := true; *} |
neuper@38009 | 13 |
(* |
neuper@38009 | 14 |
cd "systest"; |
neuper@38009 | 15 |
(*+ check kbtest/diffapp.sml for additional items in met-model*) |
neuper@38009 | 16 |
use"root-equ.sml"; |
neuper@38009 | 17 |
use"script.sml"; |
neuper@38009 | 18 |
(* use"script_if.sml"; WN03 missing: is_rootequation_in*) |
neuper@38009 | 19 |
use"scriptnew.sml"; |
neuper@38009 | 20 |
use"subp-rooteq.sml"; |
neuper@38009 | 21 |
use"tacis.sml"; |
neuper@38009 | 22 |
use"interface-xml.sml"; |
neuper@38009 | 23 |
(* use"testdaten.sml"; no update after dropping 'errorBound'*) |
neuper@38009 | 24 |
cd "../.."; |
neuper@38009 | 25 |
*) |
neuper@38009 | 26 |
ML{* writeln "**** run systests complete ******************************" *}; |
neuper@38009 | 27 |
(* |
neuper@38009 | 28 |
cd"smltest/Scripts"; |
neuper@38009 | 29 |
use"calculate-float.sml"; |
neuper@38009 | 30 |
use"calculate.sml"; |
neuper@38009 | 31 |
use"listg.sml"; |
neuper@38009 | 32 |
use"rewrite.sml"; |
neuper@38009 | 33 |
use"scrtools.sml"; |
neuper@38009 | 34 |
use"term.sml"; |
neuper@38009 | 35 |
use"tools.sml"; |
neuper@38009 | 36 |
cd "../.."; |
neuper@38009 | 37 |
cd"smltest/ME"; |
neuper@38009 | 38 |
use"ctree.sml"; |
neuper@38009 | 39 |
*) |
neuper@38009 | 40 |
use "Interpret/calchead.sml" |
neuper@38009 | 41 |
(* |
neuper@38009 | 42 |
use"calchead.sml"; |
neuper@38009 | 43 |
use"rewtools.sml"; |
neuper@38009 | 44 |
use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); |
neuper@38009 | 45 |
use"inform.sml"; |
neuper@38009 | 46 |
use"me.sml"; |
neuper@38009 | 47 |
use"ptyps.sml"; |
neuper@38009 | 48 |
cd "../.."; |
neuper@38009 | 49 |
cd"smltest/xmlsrc"; |
neuper@38009 | 50 |
use"datatypes.sml"; |
neuper@38009 | 51 |
use"pbl-met-hierarchy.sml"; |
neuper@38009 | 52 |
use"thy-hierarchy.sml"; |
neuper@38009 | 53 |
cd "../.."; |
neuper@38009 | 54 |
cd"smltest/FE-interface"; |
neuper@38009 | 55 |
use"interface.sml"; |
neuper@38009 | 56 |
cd "../.."; |
neuper@38009 | 57 |
*) |
neuper@38009 | 58 |
ML{* writeln "**** run tests on math-engine complete ******************" *}; |
neuper@38009 | 59 |
(* |
neuper@38009 | 60 |
cd"smltest/IsacKnowledge"; |
neuper@38009 | 61 |
use"atools.sml"; |
neuper@38009 | 62 |
use"complex.sml"; |
neuper@38009 | 63 |
use"diff.sml"; |
neuper@38009 | 64 |
use"diffapp.sml"; |
neuper@38010 | 65 |
*) |
neuper@38010 | 66 |
use"Knowledge/integrate.sml"; |
neuper@38010 | 67 |
(* |
neuper@38009 | 68 |
use"equation.sml"; |
neuper@38009 | 69 |
(*use"inssort.sml"; problems with recdef in Isabelle2002*) |
neuper@38009 | 70 |
use"logexp.sml"; |
neuper@38009 | 71 |
use"poly.sml"; |
neuper@38009 | 72 |
use"polyminus.sml"; |
neuper@38009 | 73 |
use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN |
neuper@38009 | 74 |
? also check others without check 'diff.behav.'*); |
neuper@38009 | 75 |
use"rateq.sml"; |
neuper@38009 | 76 |
use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*); |
neuper@38009 | 77 |
use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', |
neuper@38009 | 78 |
for simplification search MG |
neuper@38009 | 79 |
erls: 98a(1) 104a(1) 104a(2) 68a *); |
neuper@38009 | 80 |
use"root.sml"; |
neuper@38009 | 81 |
use"rooteq.sml"; |
neuper@38009 | 82 |
use"rootrateq.sml"; |
neuper@38009 | 83 |
use"termorder.sml"; |
neuper@38009 | 84 |
use"trig.sml"; |
neuper@38009 | 85 |
use"vect.sml"; |
neuper@38009 | 86 |
use"wn.sml"; |
neuper@38009 | 87 |
use"eqsystem.sml"; |
neuper@38009 | 88 |
use"biegelinie.sml"; |
neuper@38009 | 89 |
use"algein.sml"; |
neuper@38009 | 90 |
cd "../.."; |
neuper@38009 | 91 |
*) |
neuper@38009 | 92 |
ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; |
neuper@38009 | 93 |
(* |
neuper@38009 | 94 |
val path = "/home/neuper/proto2/testsml2xml/"; |
neuper@38009 | 95 |
pbl_hierarchy2file (path ^ "pbl/"); |
neuper@38009 | 96 |
pbls2file (path ^ "pbl/"); |
neuper@38009 | 97 |
met_hierarchy2file (path ^ "met/"); |
neuper@38009 | 98 |
mets2file (path ^ "met/"); |
neuper@38009 | 99 |
thy_hierarchy2file (path ^ "thy/"); |
neuper@38009 | 100 |
thes2file (path ^ "thy/"); |
neuper@38009 | 101 |
cd"sml"; |
neuper@38009 | 102 |
*) |
neuper@38009 | 103 |
ML{* writeln "**** tested creation of xmldata *************************" *}; |
neuper@37985 | 104 |
|
neuper@38009 | 105 |
ML{*states:=[]; |
neuper@38009 | 106 |
writeln "========================================================="; |
neuper@38009 | 107 |
|
neuper@38009 | 108 |
writeln "**** run systests complete ***************** re-organize!"; |
neuper@38009 | 109 |
writeln "**** run tests on math-engine complete ******************"; |
neuper@38009 | 110 |
writeln "**** run tests on IsacKnowledge complete ****************"; |
neuper@38009 | 111 |
writeln "**** build isac kernel + run tests complete *************"; |
neuper@38009 | 112 |
writeln "**** tested creation of xmldata *************************"; |
neuper@38009 | 113 |
*} |
neuper@37985 | 114 |
|
neuper@37985 | 115 |
end |