1.1 --- a/README.md Mon Dec 11 16:12:53 2023 +0100
1.2 +++ b/README.md Mon Dec 11 16:18:42 2023 +0100
1.3 @@ -58,7 +58,7 @@
1.4
1.5 * Test:
1.6
1.7 - isabisac/bin/isabelle build -D '$ISABELLE_ISAC_POS'
1.8 + isabisac/bin/isabelle build -D '$ISABELLE_ISAC_TEST'
1.9
1.10 isabisac/bin/isabelle jedit -R Isac_Test &
1.11
2.1 --- a/TODO.md Mon Dec 11 16:12:53 2023 +0100
2.2 +++ b/TODO.md Mon Dec 11 16:18:42 2023 +0100
2.3 @@ -16,7 +16,7 @@
2.4
2.5 * MW: Skip_Proof.make_thm: theory -> term -> thm ? could now change signature to
2.6 : Proof.context -> term -> thm
2.7 -* MW: Make $ISABELLE_ISAC_POS work without sessions (please synchronise with WN)
2.8 +* MW: Make $ISABELLE_ISAC_TEST work without sessions (please synchronise with WN)
2.9 * MW: ? implement a template, inserted in a proof in the line of metis;
2.10 hints are given in src/../BridgeJEdit/template.sml
2.11 and in test/../BridgeJEdit/template.sml
3.1 --- a/etc/settings Mon Dec 11 16:12:53 2023 +0100
3.2 +++ b/etc/settings Mon Dec 11 16:18:42 2023 +0100
3.3 @@ -1,4 +1,4 @@
3.4 # -*- shell-script -*- :mode=shellscript:
3.5
3.6 ISABELLE_ISAC="$COMPONENT/src/Tools/isac"
3.7 -ISABELLE_ISAC_POS="$COMPONENT/test"
3.8 +ISABELLE_ISAC_TEST="$COMPONENT/test"
4.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Dec 11 16:12:53 2023 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Dec 11 16:18:42 2023 +0100
4.3 @@ -245,7 +245,7 @@
4.4
4.5 subsubsection \<open>Specification step by step\<close>
4.6 text \<open>
4.7 - see $ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
4.8 + see $ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
4.9 \<close> ML \<open>
4.10 \<close> ML \<open>
4.11 \<close> ML \<open>
5.1 --- a/src/Tools/isac/Build_Isac.thy Mon Dec 11 16:12:53 2023 +0100
5.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Dec 11 16:18:42 2023 +0100
5.3 @@ -176,43 +176,43 @@
5.4 As first step we go top down and make Minisubpbl independent form Thy_Info here
5.5 and make sure, that the right ctxt is passed throughout the code.
5.6 As next step we go bottom up from Thy_Info.get_theory and remove it.
5.7 - Afterwards $ISABELLE_ISAC_POS will be changed accordingly.
5.8 + Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
5.9 \<close>
5.10 (** ) (* evaluated in Test_Isac/_Short *)
5.11 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/000-comments.sml"
5.12 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml"
5.13 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
5.14 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
5.15 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
5.16 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/200-start-method.sml"
5.17 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
5.18 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
5.19 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
5.20 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/300-init-subpbl.sml"
5.21 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
5.22 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
5.23 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
5.24 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml"
5.25 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/500-met-sub-to-root.sml"
5.26 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml"
5.27 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml"
5.28 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/600-postcond.sml"
5.29 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/700-interSteps.sml"
5.30 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/710-interSteps-short.sml"
5.31 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
5.32 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/790-complete.sml"
5.33 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
5.34 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
5.35 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml"
5.36 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
5.37 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
5.38 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
5.39 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
5.40 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
5.41 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
5.42 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
5.43 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
5.44 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
5.45 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
5.46 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
5.47 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml"
5.48 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/500-met-sub-to-root.sml"
5.49 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml"
5.50 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml"
5.51 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/600-postcond.sml"
5.52 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/700-interSteps.sml"
5.53 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/710-interSteps-short.sml"
5.54 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
5.55 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
5.56 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
5.57 (**)
5.58 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Specify/i-model.sml"
5.59 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Specify/i-model.sml"
5.60 (**)
5.61 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/Specify/pre-conditions.sml"
5.62 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Specify/pre-conditions.sml"
5.63
5.64 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/e-collect.sml"
5.65 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/user-model.sml"
5.66 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/template.sml"
5.67 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/preliminary.sml"
5.68 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/calculation.sml"
5.69 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/vscode-example.sml"
5.70 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/e-collect.sml"
5.71 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/user-model.sml"
5.72 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/template.sml"
5.73 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/preliminary.sml"
5.74 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
5.75 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
5.76 ( **)
5.77
5.78 (* evaluated in Test_Isac/_Short *)
5.79 @@ -255,7 +255,7 @@
5.80 unsatisfactory with respect to logical soundness.
5.81 Since Isabelle now has started to care about floating point numbers, it is high
5.82 time to adopt these together with the other numerals. Isabelle2012/13's numerals
5.83 - are different from Isabelle2011, see "$ISABELLE_ISAC_POS/Tools/isac/ProgLang/termC.sml".
5.84 + are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/termC.sml".
5.85
5.86 The transition from "Free" to standard numerals is a task to be scheduled for
5.87 several weeks. The urgency of this task follows from the experience,
6.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Dec 11 16:12:53 2023 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Dec 11 16:18:42 2023 +0100
6.3 @@ -26,7 +26,7 @@
6.4 \<^item> \<^ML>\<open>Context.get_theory\<close> for situations of explicit name-lookup (short or long)
6.5
6.6 In contrast, old-style \<^ML>\<open>Thy_Info.get_theory\<close> requires a finished logic image, for
6.7 - example in \<^file>\<open>$ISABELLE_ISAC_POS/Tools/isac/Test_Some.thy\<close> loaded from session Isac.
6.8 + example in \<^file>\<open>$ISABELLE_ISAC_TEST/Tools/isac/Test_Some.thy\<close> loaded from session Isac.
6.9
6.10 All theories below ML_structure\<open>MathEngine\<close> in the theories' dependency graph
6.11 can be considered as Isac's version of Pure: the respective code handles items
7.1 --- a/src/Tools/isac/Knowledge/gcd_poly_old.sml Mon Dec 11 16:12:53 2023 +0100
7.2 +++ b/src/Tools/isac/Knowledge/gcd_poly_old.sml Mon Dec 11 16:18:42 2023 +0100
7.3 @@ -4,7 +4,7 @@
7.4
7.5 Programcode according to [1] for later lookup for mathematicians.
7.6 The tests below remain according to [1],
7.7 -while "$ISABELLE_ISAC_POS/Tools/isac/Knowledge/gcd_poly_ml.sml" start exactly from the same state
7.8 +while "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/gcd_poly_ml.sml" start exactly from the same state
7.9 and in time follows development in "$ISABELLE_ISAC/Knowledge/GCD_Poly_ML.thy".
7.10
7.11 This file includes *** tests ***.
8.1 --- a/src/Tools/isac/Test_Code/test-code.sml Mon Dec 11 16:12:53 2023 +0100
8.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Mon Dec 11 16:18:42 2023 +0100
8.3 @@ -1,7 +1,7 @@
8.4 (* Title: Tools/isac/Testcode/test-code.sml
8.5 Author: Walther Neuper 200222
8.6
8.7 -Code used ONLY for $ISABELLE_ISAC_POS/Tools/isac/*
8.8 +Code used ONLY for $ISABELLE_ISAC_TEST/Tools/isac/*
8.9 *)
8.10
8.11 signature TEST_CODE =
9.1 --- a/test/Pure/General/Basics.thy Mon Dec 11 16:12:53 2023 +0100
9.2 +++ b/test/Pure/General/Basics.thy Mon Dec 11 16:18:42 2023 +0100
9.3 @@ -1,4 +1,4 @@
9.4 -(* Title: $ISABELLE_ISAC_POS/Pure/General/Basics.thy
9.5 +(* Title: $ISABELLE_ISAC_TEST/Pure/General/Basics.thy
9.6 Author: Walther Neuper, TU Graz, 101027
9.7 *)
9.8
10.1 --- a/test/Pure/PIDE/xml.ML Mon Dec 11 16:12:53 2023 +0100
10.2 +++ b/test/Pure/PIDE/xml.ML Mon Dec 11 16:18:42 2023 +0100
10.3 @@ -1,4 +1,4 @@
10.4 -(* Title: $ISABELLE_ISAC_POS/Pure/PIDE/xml.ML
10.5 +(* Title: $ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML
10.6 Author: Walther Neuper 1505
10.7 (c) copyright due to lincense terms.
10.8 *)
11.1 --- a/test/ROOT Mon Dec 11 16:12:53 2023 +0100
11.2 +++ b/test/ROOT Mon Dec 11 16:18:42 2023 +0100
11.3 @@ -1,25 +1,25 @@
11.4 -session Isac_Test_Base in "$ISABELLE_ISAC_POS" = HOL +
11.5 +session Isac_Test_Base in "$ISABELLE_ISAC_TEST" = HOL +
11.6 options [isac_test]
11.7 sessions Isac
11.8 theories
11.9 "Isac.Build_Isac"
11.10
11.11 -session Isac_Test in "$ISABELLE_ISAC_POS/Tools/isac" = Isac_Test_Base +
11.12 +session Isac_Test in "$ISABELLE_ISAC_TEST/Tools/isac" = Isac_Test_Base +
11.13 options [isac_test]
11.14 sessions
11.15 "HOL-Metis_Examples"
11.16 Isac
11.17 directories
11.18 - "$ISABELLE_ISAC_POS/HOL/Tools/Sledgehammer"
11.19 - "$ISABELLE_ISAC_POS/Pure"
11.20 - "$ISABELLE_ISAC_POS/Pure/General"
11.21 - "$ISABELLE_ISAC_POS/Pure/Isar"
11.22 - "$ISABELLE_ISAC_POS/Pure/PIDE"
11.23 - "$ISABELLE_ISAC_POS/Pure/Syntax"
11.24 - "$ISABELLE_ISAC_POS/Tools/isac/Knowledge"
11.25 - "$ISABELLE_ISAC_POS/Tools/isac/ProgLang"
11.26 - "$ISABELLE_ISAC_POS/Tools/isac/Specify"
11.27 - "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit"
11.28 + "$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer"
11.29 + "$ISABELLE_ISAC_TEST/Pure"
11.30 + "$ISABELLE_ISAC_TEST/Pure/General"
11.31 + "$ISABELLE_ISAC_TEST/Pure/Isar"
11.32 + "$ISABELLE_ISAC_TEST/Pure/PIDE"
11.33 + "$ISABELLE_ISAC_TEST/Pure/Syntax"
11.34 + "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge"
11.35 + "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang"
11.36 + "$ISABELLE_ISAC_TEST/Tools/isac/Specify"
11.37 + "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit"
11.38 "ADDTESTS"
11.39 "ADDTESTS/accumulate-val"
11.40 "ADDTESTS/course/phst11"
12.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Dec 11 16:12:53 2023 +0100
12.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Dec 11 16:18:42 2023 +0100
12.3 @@ -3,7 +3,7 @@
12.4 (c) due to copyright terms
12.5
12.6 this theory is evaluated BEFORE Test_Isac.thy opens structures.
12.7 - So, if you encounter errors here, first fix them in $ISABELLE_ISAC_POS/Tools/isac/Minisubpbl/* *)
12.8 + So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/* *)
12.9
12.10 theory All_Ctxt imports Isac.Build_Isac
12.11 begin
13.1 --- a/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test.thy Mon Dec 11 16:12:53 2023 +0100
13.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test.thy Mon Dec 11 16:18:42 2023 +0100
13.3 @@ -21,14 +21,14 @@
13.4 {..., Nitpick, Main, testdir1, testdirm, Build_Test}*)
13.5 imports
13.6 Complex_Main
13.7 - "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language"
13.8 - "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
13.9 + "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/1language/Foo_Language"
13.10 + "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_KnowALL"
13.11 begin
13.12 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML"
13.13 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/0foolibrary.ML"
13.14 ML \<open>val Free ("b", _) = foolibrhs @{term "a = b"}\<close>
13.15 (*use_thy "1language/Foo_Language" --- is done by import above*)
13.16 ML \<open>val Const ("Foo_Language.fooprog", _) = @{term fooprog}\<close>
13.17 - ML_file "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"
13.18 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML"
13.19 ML \<open>val Free ("b", _) = foointerpret @{term "fooprog (a = b)"}\<close>
13.20
13.21 text \<open>the different theories of knowledge are recognized, Const bar*:\<close>
14.1 --- a/test/Tools/isac/BaseDefinitions/kestore.sml Mon Dec 11 16:12:53 2023 +0100
14.2 +++ b/test/Tools/isac/BaseDefinitions/kestore.sml Mon Dec 11 16:18:42 2023 +0100
14.3 @@ -3,7 +3,7 @@
14.4 Use is subject to license terms.
14.5
14.6 theory Test_Some
14.7 - imports "Isac.Build_Isac" "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
14.8 + imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
14.9 *)
14.10
14.11 "-----------------------------------------------------------------------------";
15.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 16:12:53 2023 +0100
15.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 16:18:42 2023 +0100
15.3 @@ -4,8 +4,8 @@
15.4 begin
15.5
15.6 text \<open>
15.7 - Tests here in BridgePIDE are already based on Build_Isac.thy bypassing $ISABELLE_ISAC_POS.
15.8 - TODO: eliminate "Isac." above on eliminating session in $ISABELLE_ISAC_POS.
15.9 + Tests here in BridgePIDE are already based on Build_Isac.thy bypassing $ISABELLE_ISAC_TEST.
15.10 + TODO: eliminate "Isac." above on eliminating session in $ISABELLE_ISAC_TEST.
15.11 \<close>
15.12
15.13 subsection \<open>Development\<close>
16.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 11 16:12:53 2023 +0100
16.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 11 16:18:42 2023 +0100
16.3 @@ -5,7 +5,7 @@
16.4 theory Test_Some imports Build_Thydata begin
16.5 ML {* Know_Store.set_ref_thy @{theory};
16.6 fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
16.7 -ML_file "$ISABELLE_ISAC_POS/Tools/isac/Interpret/mathengine.sml"
16.8 +ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Interpret/mathengine.sml"
16.9 *)
16.10 "--------------------------------------------------------";
16.11 "table of contents --------------------------------------";
17.1 --- a/test/Tools/isac/Specify/refine.thy Mon Dec 11 16:12:53 2023 +0100
17.2 +++ b/test/Tools/isac/Specify/refine.thy Mon Dec 11 16:18:42 2023 +0100
17.3 @@ -97,6 +97,6 @@
17.4 \<close> ML \<open>
17.5 \<close>
17.6
17.7 -(*ML_file "$ISABELLE_ISAC_POS/Tools/isac/Specify/refine.sml" ... is called in Test_Isac.thy below,
17.8 +(*ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine.sml" ... is called in Test_Isac.thy below,
17.9 so do NOT call it HERE; circularity*)
17.10 end
18.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 11 16:12:53 2023 +0100
18.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Dec 11 16:18:42 2023 +0100
18.3 @@ -3,10 +3,10 @@
18.4 (c) copyright due to license terms.
18.5
18.6 Isac's tests are organised parallel to sources:
18.7 - $ISABELLE_ISAC_POS has same directory structure as $ISABELLE_ISAC
18.8 + $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
18.9 plus
18.10 - $ISABELLE_ISAC_POS/Tools/isac/ADDTESTS
18.11 - $ISABELLE_ISAC_POS/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
18.12 + $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
18.13 + $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
18.14
18.15 Note, that only the first error in a file is shown here.
18.16 *)
18.17 @@ -50,38 +50,38 @@
18.18 and find out, which ML_file or *.thy causes an error (might be ONLY one).
18.19 Also backup files (#* ) recognised by jEdit cause this trouble *)
18.20 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
18.21 -(* "$ISABELLE_ISAC_POS/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
18.22 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
18.23 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/Ctxt"
18.24 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/test-depend/Build_Test"
18.25 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/All_Ctxt"
18.26 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/Test_Units"
18.27 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
18.28 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
18.29 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
18.30 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
18.31 +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
18.32 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
18.33 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
18.34 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
18.35 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
18.36 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
18.37 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
18.38 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
18.39 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
18.40 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
18.41 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
18.42 ADDTESTS/------------------------------------------- see end of tests *)
18.43 (*/~~~ these work directly from Pure, but create problems here ..
18.44 - "$ISABELLE_ISAC_POS/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
18.45 - "$ISABELLE_ISAC_POS/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
18.46 - "$ISABELLE_ISAC_POS/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
18.47 - "$ISABELLE_ISAC_POS/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
18.48 - "$ISABELLE_ISAC_POS/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
18.49 + "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
18.50 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
18.51 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
18.52 + "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
18.53 + "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
18.54 \~~~ .. these work independently, but create problems here *)
18.55 -(**)"$ISABELLE_ISAC_POS/Pure/Isar/Test_Parsers"
18.56 -(**)"$ISABELLE_ISAC_POS/HOL/Tools/Sledgehammer/Try_Sledgehammer"
18.57 +(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
18.58 +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
18.59 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
18.60 - "$ISABELLE_ISAC_POS/Tools/isac/Specify/refine" (* setup for refine.sml *)
18.61 - "$ISABELLE_ISAC_POS/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
18.62 - "$ISABELLE_ISAC_POS/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
18.63 + "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
18.64 + "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
18.65 + "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
18.66 (*Test_Isac.thy*)
18.67 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
18.68 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*)
18.69 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
18.70 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
18.71 (*Test_Isac.thy*)
18.72 - "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/Test_VSCode_Example"
18.73 + "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
18.74
18.75 begin
18.76
18.77 @@ -197,10 +197,10 @@
18.78
18.79 section \<open>trials with Isabelle's functions\<close>
18.80 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
18.81 - ML_file "$ISABELLE_ISAC_POS/Pure/General/alist.ML"
18.82 - ML_file "$ISABELLE_ISAC_POS/Pure/General/basics.ML"
18.83 - ML_file "$ISABELLE_ISAC_POS/Pure/General/scan.ML"
18.84 - ML_file "$ISABELLE_ISAC_POS/Pure/PIDE/xml.ML"
18.85 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
18.86 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
18.87 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
18.88 + ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
18.89 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
18.90
18.91 section \<open>test ML Code of isac\<close>
19.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Dec 11 16:12:53 2023 +0100
19.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Dec 11 16:18:42 2023 +0100
19.3 @@ -3,10 +3,10 @@
19.4 (c) copyright due to license terms.
19.5
19.6 Isac's tests are organised parallel to sources:
19.7 - $ISABELLE_ISAC_POS has same directory structure as $ISABELLE_ISAC
19.8 + $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
19.9 plus
19.10 - $ISABELLE_ISAC_POS/Tools/isac/ADDTESTS
19.11 - $ISABELLE_ISAC_POS/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
19.12 + $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
19.13 + $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
19.14
19.15 Note, that only the first error in a file is shown here.
19.16 *)
19.17 @@ -50,38 +50,38 @@
19.18 and find out, which ML_file or *.thy causes an error (might be ONLY one).
19.19 Also backup files (#* ) recognised by jEdit cause this trouble *)
19.20 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
19.21 -(* "$ISABELLE_ISAC_POS/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
19.22 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
19.23 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/Ctxt"
19.24 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/test-depend/Build_Test"
19.25 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/All_Ctxt"
19.26 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/Test_Units"
19.27 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
19.28 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
19.29 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
19.30 -(**)"$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
19.31 +(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
19.32 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
19.33 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
19.34 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
19.35 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
19.36 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
19.37 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
19.38 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
19.39 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
19.40 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
19.41 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
19.42 ADDTESTS/------------------------------------------- see end of tests *)
19.43 (*/~~~ these work directly from Pure, but create problems here ..
19.44 - "$ISABELLE_ISAC_POS/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
19.45 - "$ISABELLE_ISAC_POS/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
19.46 - "$ISABELLE_ISAC_POS/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
19.47 - "$ISABELLE_ISAC_POS/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
19.48 - "$ISABELLE_ISAC_POS/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
19.49 + "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
19.50 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
19.51 + "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
19.52 + "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
19.53 + "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
19.54 \~~~ .. these work independently, but create problems here *)
19.55 -(**)"$ISABELLE_ISAC_POS/Pure/Isar/Test_Parsers"
19.56 -(**)"$ISABELLE_ISAC_POS/HOL/Tools/Sledgehammer/Try_Sledgehammer"
19.57 +(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
19.58 +(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
19.59 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
19.60 - "$ISABELLE_ISAC_POS/Tools/isac/Specify/refine" (* setup for refine.sml *)
19.61 - "$ISABELLE_ISAC_POS/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
19.62 - "$ISABELLE_ISAC_POS/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
19.63 + "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
19.64 + "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
19.65 + "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
19.66 (*Test_Isac_Short.thy* )
19.67 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
19.68 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
19.69 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
19.70 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
19.71 ( *Test_Isac_Short.thy*)
19.72 - "$ISABELLE_ISAC_POS/Tools/isac/BridgeJEdit/Test_VSCode_Example"
19.73 + "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
19.74
19.75 begin
19.76
19.77 @@ -197,10 +197,10 @@
19.78
19.79 section \<open>trials with Isabelle's functions\<close>
19.80 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
19.81 - ML_file "$ISABELLE_ISAC_POS/Pure/General/alist.ML"
19.82 - ML_file "$ISABELLE_ISAC_POS/Pure/General/basics.ML"
19.83 - ML_file "$ISABELLE_ISAC_POS/Pure/General/scan.ML"
19.84 - ML_file "$ISABELLE_ISAC_POS/Pure/PIDE/xml.ML"
19.85 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
19.86 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
19.87 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
19.88 + ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
19.89 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
19.90
19.91 section \<open>test ML Code of isac\<close>
20.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 11 16:12:53 2023 +0100
20.2 +++ b/test/Tools/isac/Test_Some.thy Mon Dec 11 16:18:42 2023 +0100
20.3 @@ -1,5 +1,5 @@
20.4 theory Test_Some
20.5 - imports "Isac.Build_Isac" "$ISABELLE_ISAC_POS/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
20.6 + imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
20.7 begin
20.8
20.9 ML \<open>open ML_System\<close>
21.1 --- a/test/Tools/isac/Test_Theory.thy Mon Dec 11 16:12:53 2023 +0100
21.2 +++ b/test/Tools/isac/Test_Theory.thy Mon Dec 11 16:18:42 2023 +0100
21.3 @@ -1,6 +1,6 @@
21.4 (* use this theory for tests before Build_Isac.thy has succeeded *)
21.5 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"
21.6 - "$ISABELLE_ISAC_POS/Tools/isac/Specify/refine" (* setup for refine.sml *)
21.7 + "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
21.8 begin
21.9 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
21.10