1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) |
1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) |
2 Author: Walther Neuper 101001 |
2 Author: Walther Neuper 101001 |
3 (c) copyright due to license terms. |
3 (c) copyright due to license terms. |
4 |
4 |
5 Isac's tests are organised parallel to sources: |
5 Isac's tests are organised parallel to sources: |
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" |
6 $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC |
7 plus |
7 plus |
8 ~~/test/Tools/isac/ADDTESTS |
8 $ISABELLE_ISAC_TEST/ADDTESTS |
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality |
9 $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality |
10 |
10 |
11 Note, that only the first error in a file is shown here. |
11 Note, that only the first error in a file is shown here. |
12 *) |
12 *) |
13 |
13 |
14 section \<open>Notes on running tests\<close> |
14 section \<open>Notes on running tests\<close> |
59 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) |
59 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) |
60 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one |
60 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one |
61 and find out, which ML_file or *.thy causes an error (might be ONLY one). |
61 and find out, which ML_file or *.thy causes an error (might be ONLY one). |
62 Also backup files (#* ) recognised by jEdit cause this trouble *) |
62 Also backup files (#* ) recognised by jEdit cause this trouble *) |
63 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
63 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
64 "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" |
64 "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All" |
65 (**)"~~/test/Tools/isac/ADDTESTS/Ctxt" |
65 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt" |
66 (**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" |
66 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test" |
67 (**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt" |
67 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt" |
68 (**)"~~/test/Tools/isac/ADDTESTS/Test_Units" |
68 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units" |
69 (**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" |
69 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics" |
70 (**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" |
70 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting" |
71 (**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" |
71 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine" |
72 (**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" |
72 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test" |
73 (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" |
73 (**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo" |
74 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
74 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
75 ADDTESTS/------------------------------------------- see end of tests *) |
75 ADDTESTS/------------------------------------------- see end of tests *) |
76 (*/--- these work directly from Pure, but create problems here .. |
76 (*/--- these work directly from Pure, but create problems here .. |
77 "~~/test/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *) |
77 "~~/test/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *) |
78 "~~/test/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *) |
78 "~~/test/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *) |
82 \--- .. these work independently, but create problems here *) |
82 \--- .. these work independently, but create problems here *) |
83 (**)"~~/test/Pure/Isar/Check_Outer_Syntax" |
83 (**)"~~/test/Pure/Isar/Check_Outer_Syntax" |
84 (**)"~~/test/Pure/Isar/Test_Parsers" |
84 (**)"~~/test/Pure/Isar/Test_Parsers" |
85 (**)"~~/test/Pure/Isar/Test_Parse_Term" |
85 (**)"~~/test/Pure/Isar/Test_Parse_Term" |
86 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
86 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
87 "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *) |
87 "$ISABELLE_ISAC_TEST/Specify/refine" (* setup for refine.sml *) |
88 "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *) |
88 "$ISABELLE_ISAC_TEST/ProgLang/calculate" (* setup for evaluate.sml *) |
89 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) |
89 "$ISABELLE_ISAC_TEST/Knowledge/integrate" (* setup for integrate.sml*) |
90 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
90 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
91 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) |
91 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) |
92 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) |
92 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) |
93 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
93 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
94 |
94 |
95 begin |
95 begin |
96 |
96 |
97 ML \<open>open ML_System\<close> |
97 ML \<open>open ML_System\<close> |
360 |
360 |
361 ML_file "Test_Code/test-code.sml" |
361 ML_file "Test_Code/test-code.sml" |
362 |
362 |
363 section \<open>further tests additional to src/.. files\<close> |
363 section \<open>further tests additional to src/.. files\<close> |
364 ML_file "BridgeLibisabelle/use-cases.sml" |
364 ML_file "BridgeLibisabelle/use-cases.sml" |
365 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" |
365 ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml" |
366 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" |
366 ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml" |
367 |
367 |
368 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
368 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
369 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
369 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
370 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
370 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
371 ML \<open> |
371 ML \<open> |
509 subsubsection \<open>Summary of development\<close> |
509 subsubsection \<open>Summary of development\<close> |
510 text \<open> |
510 text \<open> |
511 isac on Isabelle2012 is considered just a transitional stage |
511 isac on Isabelle2012 is considered just a transitional stage |
512 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; |
512 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; |
513 For considerations on the transition see |
513 For considerations on the transition see |
514 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..". |
514 $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..". |
515 \<close> |
515 \<close> |
516 subsubsection \<open>Run tests\<close> |
516 subsubsection \<open>Run tests\<close> |
517 text \<open> |
517 text \<open> |
518 $ cd /usr/local/isabisac12/ |
518 $ cd /usr/local/isabisac12/ |
519 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy |
519 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy |