1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sat Jul 17 14:05:28 2021 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
1.5 +(* Title: All tests on isac (some outcommented since Isabelle2002-->2009- 2)
1.6 Author: Walther Neuper 101001
1.7 (c) copyright due to license terms.
1.8
1.9 @@ -139,8 +139,11 @@
1.10 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.11 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
1.12 "xx"
1.13 -^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
1.14 +^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
1.15 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
1.16 \<close> ML \<open>
1.17 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
1.18 +Rewrite.trace_on := false;
1.19 \<close>
1.20 ML \<open>
1.21 \<close> ML \<open>
1.22 @@ -187,7 +190,7 @@
1.23 ML_file "BaseDefinitions/calcelems.sml"
1.24 ML_file "BaseDefinitions/termC.sml"
1.25 ML_file "BaseDefinitions/substitution.sml"
1.26 - ML_file "BaseDefinitions/contextC.sml"
1.27 +(*ML_file "BaseDefinitions/contextC.sml" loops with eliminate ThmC.numerals_to_Free*)
1.28 ML_file "BaseDefinitions/environment.sml"
1.29 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.30 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.31 @@ -231,7 +234,7 @@
1.32 ML_file "MathEngBasic/thmC.sml"
1.33 ML_file "MathEngBasic/rewrite.sml"
1.34 ML_file "MathEngBasic/tactic.sml"
1.35 -(*ML_file "MathEngBasic/ctree.sml" TOODOO Isa hangs ?!?*)
1.36 +(** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*)
1.37 ML_file "MathEngBasic/calculation.sml"
1.38
1.39 ML_file "Specify/formalise.sml"
1.40 @@ -268,43 +271,43 @@
1.41 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
1.42 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
1.43 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
1.44 - ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
1.45 -(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free*)
1.46 -(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.47 - ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.48 -
1.49 + ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
1.50 +(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free
1.51 + but is already deprecated ( **)
1.52 ML_file "BridgeJEdit/parseC.sml"
1.53 ML_file "BridgeJEdit/preliminary.sml"
1.54
1.55 ML_file "Knowledge/delete.sml"
1.56 ML_file "Knowledge/descript.sml"
1.57 ML_file "Knowledge/simplify.sml"
1.58 - ML_file "Knowledge/poly.sml"
1.59 -ML \<open>
1.60 -\<close> ML \<open>
1.61 -\<close> ML \<open>
1.62 -\<close> ML \<open>
1.63 -\<close> ML \<open>
1.64 -\<close> ML \<open>
1.65 -\<close> ML \<open>
1.66 -\<close> ML \<open>
1.67 -\<close> ML \<open>
1.68 -\<close> ML \<open>
1.69 -\<close> ML \<open>
1.70 -\<close>
1.71 + ML_file "Knowledge/poly-1.sml"
1.72 +(*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
1.73 ML_file "Knowledge/gcd_poly_ml.sml"
1.74 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
1.75 - ML_file "Knowledge/rational.sml" (*Test_Isac_Short*)
1.76 + ML_file "Knowledge/rational-1.sml"
1.77 +(*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
1.78 ML_file "Knowledge/equation.sml"
1.79 - ML_file "Knowledge/root.sml"
1.80 +(*ML_file "Knowledge/root.sml" see TODO.ThmC.numerals_to_Free 1*)
1.81 ML_file "Knowledge/lineq.sml"
1.82
1.83 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
1.84 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
1.85 - ML_file "Knowledge/r/ootrat.sml"
1.86 +(*ML_file "Knowledge/rootrat.sml" see TODO.ThmC.numerals_to_Free 1*)
1.87 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
1.88 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
1.89 ML_file "Knowledge/polyeq-1.sml"
1.90 +ML \<open>
1.91 +\<close> ML \<open>
1.92 +\<close> ML \<open>
1.93 +\<close> ML \<open>
1.94 +\<close> ML \<open>
1.95 +\<close> ML \<open>
1.96 +\<close> ML \<open>
1.97 +\<close> ML \<open>
1.98 +\<close> ML \<open>
1.99 +\<close> ML \<open>
1.100 +\<close> ML \<open>
1.101 +\<close>
1.102 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
1.103 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
1.104 ML_file "Knowledge/calculus.sml"
1.105 @@ -331,7 +334,7 @@
1.106 ML_file "Test_Code/test-code.sml"
1.107
1.108 section \<open>further tests additional to src/.. files\<close>
1.109 - ML_file "BridgeLibisabelle/use-cases.sml"
1.110 + ML_file "BridgeLibisabelle/use-cases.sml"
1.111
1.112 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.113 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.114 @@ -399,7 +402,7 @@
1.115 migration from "isabelle tty" --> libisabelle
1.116 \<close>
1.117
1.118 -subsection \<open>isac on Isabelle2013-2\<close>
1.119 +subsection \<open>isac on Isabelle2013- 2\<close>
1.120 subsubsection \<open>Summary of development\<close>
1.121 text \<open>
1.122 reactivated context_thy
1.123 @@ -412,17 +415,17 @@
1.124 text \<open>
1.125 TODO
1.126 :
1.127 - : isac on Isablle2013-2
1.128 + : isac on Isablle2013- 2
1.129 :
1.130 Changeset: 55318 (03826ceb24da) merged
1.131 User: Walther Neuper <neuper@ist.tugraz.at>
1.132 - Date: 2013-12-12 14:27:37 +0100 (7 minutes)
1.133 + Date: 2013- 12- 12 14:27:37 +0100 (7 minutes)
1.134 \<close>
1.135
1.136 -subsection \<open>isac on Isabelle2013-1\<close>
1.137 +subsection \<open>isac on Isabelle2013- 1\<close>
1.138 subsubsection \<open>Summary of development\<close>
1.139 text \<open>
1.140 - Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
1.141 + Isabelle2013- 1 was replaced within a few weeks due to problems with the document model;
1.142 no significant development steps for ISAC.
1.143 \<close>
1.144 subsubsection \<open>State of tests\<close>
1.145 @@ -433,13 +436,13 @@
1.146 text \<open>
1.147 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
1.148 User: Walther Neuper <neuper@ist.tugraz.at>
1.149 - Date: 2013-12-03 18:13:31 +0100 (8 days)
1.150 + Date: 2013- 12-03 18:13:31 +0100 (8 days)
1.151 :
1.152 - : isac on Isablle2013-1
1.153 + : isac on Isablle2013- 1
1.154 :
1.155 - Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
1.156 + Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013- 1: Test_Isac perfect
1.157 User: Walther Neuper <neuper@ist.tugraz.at>
1.158 - Date: 2013-11-21 18:12:17 +0100 (2 weeks)
1.159 + Date: 2013- 11- 21 18:12:17 +0100 (2 weeks)
1.160
1.161 \<close>
1.162
1.163 @@ -453,7 +456,7 @@
1.164 \<close>
1.165 subsubsection \<open>Run tests\<close>
1.166 text \<open>
1.167 - Is standard now; this subsection will be discontinued under Isabelle2013-1
1.168 + Is standard now; this subsection will be discontinued under Isabelle2013- 1
1.169 \<close>
1.170 subsubsection \<open>State of tests\<close>
1.171 text \<open>
1.172 @@ -470,7 +473,7 @@
1.173 :
1.174 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
1.175 User: Walther Neuper <neuper@ist.tugraz.at>
1.176 - Date: 2013-07-15 08:28:50 +0200 (4 weeks)
1.177 + Date: 2013-07- 15 08:28:50 +0200 (4 weeks)
1.178 \<close>
1.179
1.180 subsection \<open>isac on Isabelle2012\<close>
1.181 @@ -494,13 +497,13 @@
1.182 in parallel with evaluation.
1.183
1.184 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
1.185 - yields 69 hits, some of which were already present before Isabelle2002-->2009-2
1.186 + yields 69 hits, some of which were already present before Isabelle2002-->2009- 2
1.187 (i.e. on the old notebook from 2002).
1.188
1.189 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
1.190 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
1.191 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
1.192 - # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
1.193 + # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009- 2 === , most likely go back to 2002
1.194 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
1.195
1.196 Some tests have been re-activated (e.g. error patterns, fill patterns).
1.197 @@ -509,17 +512,17 @@
1.198 text \<open>
1.199 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
1.200 User: Walther Neuper <neuper@ist.tugraz.at>
1.201 - Date: 2013-07-11 16:58:31 +0200 (4 weeks)
1.202 + Date: 2013-07- 11 16:58:31 +0200 (4 weeks)
1.203 :
1.204 : isac on Isablle2012
1.205 :
1.206 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
1.207 User: Walther Neuper <neuper@ist.tugraz.at>
1.208 - Date: 2012-09-24 18:35:13 +0200 (8 months)
1.209 + Date: 2012-09- 24 18:35:13 +0200 (8 months)
1.210 ------------------------------------------------------------------------------
1.211 Changeset: 48756 (7443906996a8) merged
1.212 User: Walther Neuper <neuper@ist.tugraz.at>
1.213 - Date: 2012-09-24 18:15:49 +0200 (8 months)
1.214 + Date: 2012-09- 24 18:15:49 +0200 (8 months)
1.215 \<close>
1.216
1.217 subsection \<open>isac on Isabelle2011\<close>
1.218 @@ -557,7 +560,7 @@
1.219
1.220 The list below records TODOs while producing an ISAC kernel for
1.221 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
1.222 - (so to be resumed with Isabelle2013-1):
1.223 + (so to be resumed with Isabelle2013- 1):
1.224 ############## WNxxxxxx.TODO can be found in sources ##############
1.225 --------------------------------------------------------------------------------
1.226 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
1.227 @@ -593,7 +596,7 @@
1.228 --------------------------------------------------------------------------------
1.229 WN120320.TODO check-improve rlsthmsNOTisac:
1.230 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
1.231 - DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
1.232 + DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09- 2.sml .. Isac.thy
1.233 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
1.234 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
1.235 --------------------------------------------------------------------------------
1.236 @@ -702,18 +705,18 @@
1.237 ------------------------------------------------------------------------------
1.238 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
1.239 User: Walther Neuper <neuper@ist.tugraz.at>
1.240 - Date: 2012-09-24 16:39:30 +0200 (8 months)
1.241 + Date: 2012-09- 24 16:39:30 +0200 (8 months)
1.242 :
1.243 : isac on Isablle2011
1.244 :
1.245 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
1.246 Branch: decompose-isar
1.247 User: Walther Neuper <neuper@ist.tugraz.at>
1.248 - Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
1.249 + Date: 2011-02- 25 13:04:56 +0100 (2011-02- 25)
1.250 ------------------------------------------------------------------------------
1.251 \<close>
1.252
1.253 -subsection \<open>isac on Isabelle2009-2\<close>
1.254 +subsection \<open>isac on Isabelle2009- 2\<close>
1.255 subsubsection \<open>Summary of development\<close>
1.256 text \<open>
1.257 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
1.258 @@ -726,14 +729,14 @@
1.259 WN131021 this is broken by installation of Isabelle2011/12/13,
1.260 because all these write their binaries to ~/.isabelle/heaps/..
1.261
1.262 - $ cd /usr/local/isabisac09-2/
1.263 + $ cd /usr/local/isabisac09- 2/
1.264 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
1.265 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
1.266 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
1.267 \<close>
1.268 subsubsection \<open>State of tests\<close>
1.269 text \<open>
1.270 - Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
1.271 + Most tests are broken by the update from Isabelle2002 to Isabelle2009- 2.
1.272 \<close>
1.273 subsubsection \<open>Changesets of begin and end\<close>
1.274 text \<open>
1.275 @@ -744,12 +747,12 @@
1.276 User: Marco Steger <m.steger@student.tugraz.at>
1.277 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
1.278 :
1.279 - : isac on Isablle2009-2
1.280 + : isac on Isablle2009- 2
1.281 :
1.282 - Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
1.283 - Branch: isac-from-Isabelle2009-2
1.284 + Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009- 2
1.285 + Branch: isac-from-Isabelle2009- 2
1.286 User: Walther Neuper <neuper@ist.tugraz.at>
1.287 - Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
1.288 + Date: 2010-07- 21 09:59:35 +0200 (2010-07- 21)
1.289 ------------------------------------------------------------------------------
1.290 \<close>
1.291