1.1 --- a/test/Tools/isac/Test_Isac.thy Fri Apr 16 22:13:43 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Apr 16 22:29:23 2021 +0200
1.3 @@ -3,10 +3,10 @@
1.4 (c) copyright due to license terms.
1.5
1.6 Isac's tests are organised parallel to sources:
1.7 - "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
1.8 + $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
1.9 plus
1.10 - ~~/test/Tools/isac/ADDTESTS
1.11 - ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
1.12 + $ISABELLE_ISAC_TEST/ADDTESTS
1.13 + $ISABELLE_ISAC_TEST/Minisubpbl: the Lucas-Interpreter's core functionality
1.14
1.15 Note, that only the first error in a file is shown here.
1.16 *)
1.17 @@ -61,16 +61,16 @@
1.18 and find out, which ML_file or *.thy causes an error (might be ONLY one).
1.19 Also backup files (#* ) recognised by jEdit cause this trouble *)
1.20 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.21 - "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
1.22 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
1.23 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
1.24 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
1.25 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
1.26 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
1.27 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
1.28 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
1.29 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
1.30 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
1.31 + "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"
1.32 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Ctxt"
1.33 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/test-depend/Build_Test"
1.34 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/All_Ctxt"
1.35 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/Test_Units"
1.36 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T1_Basics"
1.37 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T2_Rewriting"
1.38 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/course/phst11/T3_MathEngine"
1.39 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/file-depend/BuildC_Test"
1.40 +(**)"$ISABELLE_ISAC_TEST/ADDTESTS/session-get_theory/Foo"
1.41 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.42 ADDTESTS/------------------------------------------- see end of tests *)
1.43 (*/--- these work directly from Pure, but create problems here ..
1.44 @@ -84,12 +84,12 @@
1.45 (**)"~~/test/Pure/Isar/Test_Parsers"
1.46 (**)"~~/test/Pure/Isar/Test_Parse_Term"
1.47 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.48 - "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
1.49 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
1.50 - "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
1.51 + "$ISABELLE_ISAC_TEST/Specify/refine" (* setup for refine.sml *)
1.52 + "$ISABELLE_ISAC_TEST/ProgLang/calculate" (* setup for evaluate.sml *)
1.53 + "$ISABELLE_ISAC_TEST/Knowledge/integrate" (* setup for integrate.sml*)
1.54 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.55 - "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
1.56 - "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
1.57 + "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
1.58 + "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
1.59 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.60
1.61 begin
1.62 @@ -362,8 +362,8 @@
1.63
1.64 section \<open>further tests additional to src/.. files\<close>
1.65 ML_file "BridgeLibisabelle/use-cases.sml"
1.66 - ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
1.67 - ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
1.68 + ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/mini-test.sml"
1.69 + ML_file "$ISABELLE_ISAC_TEST/ADDTESTS/libisabelle/protocol.sml"
1.70
1.71 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.72 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.73 @@ -511,7 +511,7 @@
1.74 isac on Isabelle2012 is considered just a transitional stage
1.75 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
1.76 For considerations on the transition see
1.77 - ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
1.78 + $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
1.79 \<close>
1.80 subsubsection \<open>Run tests\<close>
1.81 text \<open>