1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 16 19:39:48 2019 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Sep 16 20:40:33 2019 +0200
1.3 @@ -7,37 +7,43 @@
1.4 plus
1.5 ~~/test/Tools/isac/ADDTESTS
1.6 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
1.7 --------------------------------------------------------------------------------
1.8 -
1.9 -Prepare running tests: see below
1.10 -Run tests:
1.11 -$ cd /usr/local/isabisac/
1.12 -$ export ISABELLE_VERSION=2015 # for libisabelle
1.13 -$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
1.14 *)
1.15
1.16 -section \<open>Prepare running tests\<close>
1.17 +section \<open>Notes on running tests\<close>
1.18 +subsection \<open>Switch between running tests and updating code\<close>
1.19 text \<open>
1.20 -Isac encapsulates code as much as possible in structures without open. TODO ProgLang.
1.21 -This policy conflicts with those tests, which go into functions to details
1.22 -not declared in the signatures.
1.23 + Isac encapsulates code as much as possible in structures without open.
1.24 + This policy conflicts with those tests, which go into functions to details
1.25 + not declared in the signatures.
1.26 +
1.27 + In order to maintain these tests without changes, this has to be done before running tests:
1.28 + (1) Extend signatures for tests by
1.29 + ~~$ ./xcoding-to-test.sh
1.30 + ~~$ ./zcoding-to-test.sh # --"-- + go back to Test_Isac.thy
1.31 + Running Test_Isac.thy opens all structures, see code after "begin" below.
1.32 + (2) Clean signatures for coding
1.33 + ~~$ ./xtest-to-coding.sh
1.34 + ~~$ ./ztest-to-coding.sh # --"-- + go back to coding (!update thy!)
1.35
1.36 -In order to maintain these tests without changes, this has to be done before running tests:
1.37 -(1) Extend signatures for tests by
1.38 - ~~$ ./xcoding-to-test.sh
1.39 - ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy
1.40 - Running Test_Isac.thy opens all structures, see code after "begin" below.
1.41 -(2) Clean signatures for coding
1.42 - ~~$ ./xtest-to-coding.sh
1.43 - ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!)
1.44 +********************* don't forget (2) BEFORE pushing to repository ****************************
1.45 +\<close>
1.46 +subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
1.47 +text \<open>
1.48 + Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
1.49 + if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
1.50 + This exception can be avoided by ML_system_64 = "true" in ~~/etc/preferences.
1.51 + These preferences have drawbacks, however:
1.52 + * they claim more memory such that Isabelle instances canNOT run in parallel.
1.53 + * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
1.54
1.55 -********************* don't forget (2) BEFORE pushing to repository *********************
1.56 + So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
1.57 + From time to time full testing in Test_Isac.thy is recommended. For that purpose
1.58 + * set ML_system_64 = "true"
1.59
1.60 -The above bash files accomplish query replace in src/Tools/isac:
1.61 - \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
1.62 - \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit> \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
1.63 - ^^^ in signature outcommented, ^^^ NOT outcommented,
1.64 - this is status for coding this is status for tests
1.65 +********************* don't forget to re-set defaults BEFORE updating code *********************
1.66 +
1.67 + Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always
1.68 + ******* edit etc/preferences by use of gedit *******
1.69 \<close>
1.70
1.71 section \<open>code for copy & paste\<close>
1.72 @@ -53,7 +59,7 @@
1.73 * watch the <Theories> window for errors in the "imports" below
1.74 \<close>
1.75
1.76 -theory Test_Isac_Short
1.77 +theory Test_Isac_Short
1.78 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
1.79 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.80 "ADDTESTS/accumulate-val/Thy_All"
1.81 @@ -157,6 +163,7 @@
1.82 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
1.83 ML_file "ProgLang/rewrite.sml"
1.84 ML_file "ProgLang/scrtools.sml"
1.85 + ML_file "ProgLang/tools.sml"
1.86 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.87 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.88
1.89 @@ -217,11 +224,11 @@
1.90 ML_file "Knowledge/root.sml"
1.91 ML_file "Knowledge/lineq.sml"
1.92 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
1.93 -(*ML_file "Knowledge/rateq.sml" ( *some complicated equations not rec.f.2002 Test_Isac_Short*)
1.94 +(*ML_file "Knowledge/rateq.sml" some complicated.eq... exception Size---Test_Isac_Short*)
1.95 ML_file "Knowledge/rootrat.sml"
1.96 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
1.97 - ML_file "Knowledge/partial_fractions.sml"(* exception Size raised "./basis/LibrarySupport.sml"*)
1.98 -(*ML_file "Knowledge/polyeq.sml" Test_Isac_Short*)
1.99 +(*ML_file "Knowledge/partial_fractions.sml" exception Size---Test_Isac_Short*)
1.100 +(*ML_file "Knowledge/polyeq.sml" exception Size---Test_Isac_Short*)
1.101 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
1.102 ML_file "Knowledge/calculus.sml"
1.103 ML_file "Knowledge/trig.sml"
1.104 @@ -233,12 +240,12 @@
1.105 ML_file "Knowledge/polyminus.sml"
1.106 ML_file "Knowledge/vect.sml"
1.107 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
1.108 - ML_file "Knowledge/biegelinie-1.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
1.109 -(*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
1.110 + ML_file "Knowledge/biegelinie-1.sml"
1.111 +(*ML_file "Knowledge/biegelinie-2.sml" exception Size---Test_Isac_Short*)
1.112 ML_file "Knowledge/biegelinie-3.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
1.113 ML_file "Knowledge/algein.sml"
1.114 ML_file "Knowledge/diophanteq.sml"
1.115 - ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
1.116 +(*ML_file "Knowledge/inverse_z_transform.sml" exception Size---Test_Isac_Short*)
1.117 ML_file "Knowledge/inssort.sml"
1.118 ML_file "Knowledge/isac.sml"
1.119 ML_file "Knowledge/build_thydata.sml"