1.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 12 06:37:04 2020 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 12 07:27:21 2020 +0200
1.3 @@ -27,7 +27,7 @@
1.4 ~~$ ./xtest-to-coding.sh
1.5 ~~$ ./ztest-to-coding.sh # --"-- + go back to coding (!update thy!)
1.6
1.7 -********************* don't forget (2) BEFORE pushing to repository ****************************
1.8 +//******************* don't forget (2) BEFORE pushing to repository **************************\\
1.9 \<close>
1.10 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
1.11 text \<open>
1.12 @@ -43,7 +43,7 @@
1.13 From time to time full testing in Test_Isac.thy is recommended. For that purpose
1.14 * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
1.15
1.16 -********************* don't forget to re-set defaults BEFORE updating code *********************
1.17 +\\******************* don't forget to re-set defaults BEFORE updating code *******************//
1.18
1.19 Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
1.20 ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
1.21 @@ -57,25 +57,26 @@
1.22
1.23 theory Test_Isac
1.24 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
1.25 + (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one *)
1.26 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.27 - "ADDTESTS/accumulate-val/Thy_All"
1.28 - "ADDTESTS/Ctxt"
1.29 - "ADDTESTS/test-depend/Build_Test"
1.30 - "ADDTESTS/All_Ctxt"
1.31 - "ADDTESTS/Test_Units"
1.32 - "ADDTESTS/course/phst11/T1_Basics"
1.33 - "ADDTESTS/course/phst11/T2_Rewriting"
1.34 - "ADDTESTS/course/phst11/T3_MathEngine"
1.35 - "ADDTESTS/file-depend/BuildC_Test"
1.36 - "ADDTESTS/session-get_theory/Foo"
1.37 + "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" (*broken with 05944144a692 *)
1.38 +(**)"~~/test/Tools/isac/ADDTESTS/Ctxt" (*broken with 05944144a692 *)
1.39 +(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" (*broken with 05944144a692 *)
1.40 +(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt" (*broken with 05944144a692 *)
1.41 +(**)"~~/test/Tools/isac/ADDTESTS/Test_Units" (*broken with 05944144a692 *)
1.42 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" (*broken with 05944144a692 *)
1.43 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" (*broken with 05944144a692 *)
1.44 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"(*broken with 05944144a692 *)
1.45 +(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" (*broken with 05944144a692 *)
1.46 +(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" (*broken with 05944144a692 *)
1.47 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.48 ADDTESTS/------------------------------------------- see end of tests *)
1.49 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
1.50 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
1.51 - "~~/test/Pure/Isar/Test_Parse_Term"
1.52 +(**)"~~/test/Pure/Isar/Test_Parse_Term" (*broken with 05944144a692 *)
1.53 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.54 - "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
1.55 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml*)
1.56 + "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
1.57 + "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
1.58 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
1.59 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
1.60 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
1.61 @@ -117,7 +118,6 @@
1.62 open Step_Solve;
1.63 open Step;
1.64 open Solve; (* NONE *)
1.65 - open Stool; (* NONE *)
1.66 open ContextC; transfer_asms_from_to;
1.67 open Tactic; (* NONE *)
1.68 open P_Model; (* NONE *)
1.69 @@ -191,11 +191,11 @@
1.70 ML_file "BaseDefinitions/substitution.sml"
1.71 ML_file "BaseDefinitions/contextC.sml"
1.72 ML_file "BaseDefinitions/environment.sml"
1.73 - ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.74 + ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.75 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.76 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.77
1.78 - ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
1.79 + ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
1.80 ML_file "ProgLang/listC.sml"
1.81 ML_file "ProgLang/prog_expr.sml"
1.82 ML_file "ProgLang/program.sml"
1.83 @@ -231,7 +231,6 @@
1.84 subsection \<open>further functionality alongside batch build sequence\<close>
1.85 ML_file "MathEngBasic/thmC.sml"
1.86 ML_file "MathEngBasic/rewrite.sml"
1.87 - ML_file "MathEngBasic/model.sml"
1.88 (*ML_file "MathEngBasic/mstools.sml"*)
1.89 ML_file "MathEngBasic/tactic.sml"
1.90 ML_file "MathEngBasic/ctree.sml"
1.91 @@ -239,9 +238,10 @@
1.92
1.93 ML_file "Specify/o-model.sml"
1.94 ML_file "Specify/i-model.sml"
1.95 - ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
1.96 + ML_file "Specify/model.sml"
1.97 + ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
1.98 + ML_file "Specify/ptyps.sml"
1.99 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
1.100 - ML_file "Specify/generate.sml"
1.101 ML_file "Specify/calchead.sml"
1.102 ML_file "Specify/step-specify.sml"
1.103 ML_file "Specify/specify.sml"