1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 24 16:47:31 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu May 26 12:44:51 2022 +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 @@ -166,7 +166,7 @@
1.10
1.11 section \<open>trials with Isabelle's functions\<close>
1.12 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.13 - ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.14 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.15 ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
1.16 ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
1.17 ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
1.18 @@ -190,9 +190,9 @@
1.19 ML_file "BaseDefinitions/calcelems.sml"
1.20 ML_file "BaseDefinitions/termC.sml"
1.21 ML_file "BaseDefinitions/substitution.sml"
1.22 - ML_file "BaseDefinitions/contextC.sml"
1.23 + ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
1.24 ML_file "BaseDefinitions/environment.sml"
1.25 -(** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.26 +(**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
1.27 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.28 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.29
1.30 @@ -271,7 +271,7 @@
1.31 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
1.32 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
1.33 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
1.34 - ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
1.35 + ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
1.36 ML_file "BridgeLibisabelle/interface.sml"
1.37 ML_file "BridgeJEdit/parseC.sml"
1.38 ML_file "BridgeJEdit/preliminary.sml"
1.39 @@ -389,7 +389,7 @@
1.40 migration from "isabelle tty" --> libisabelle
1.41 \<close>
1.42
1.43 -subsection \<open>isac on Isabelle2013- 2\<close>
1.44 +subsection \<open>isac on Isabelle2013-2\<close>
1.45 subsubsection \<open>Summary of development\<close>
1.46 text \<open>
1.47 reactivated context_thy
1.48 @@ -402,17 +402,17 @@
1.49 text \<open>
1.50 TODO
1.51 :
1.52 - : isac on Isablle2013- 2
1.53 + : isac on Isablle2013-2
1.54 :
1.55 Changeset: 55318 (03826ceb24da) merged
1.56 User: Walther Neuper <neuper@ist.tugraz.at>
1.57 - Date: 2013- 12- 12 14:27:37 +0100 (7 minutes)
1.58 + Date: 2013-12-12 14:27:37 +0100 (7 minutes)
1.59 \<close>
1.60
1.61 -subsection \<open>isac on Isabelle2013- 1\<close>
1.62 +subsection \<open>isac on Isabelle2013-1\<close>
1.63 subsubsection \<open>Summary of development\<close>
1.64 text \<open>
1.65 - Isabelle2013- 1 was replaced within a few weeks due to problems with the document model;
1.66 + Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
1.67 no significant development steps for ISAC.
1.68 \<close>
1.69 subsubsection \<open>State of tests\<close>
1.70 @@ -423,13 +423,13 @@
1.71 text \<open>
1.72 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
1.73 User: Walther Neuper <neuper@ist.tugraz.at>
1.74 - Date: 2013- 12-03 18:13:31 +0100 (8 days)
1.75 + Date: 2013-12-03 18:13:31 +0100 (8 days)
1.76 :
1.77 - : isac on Isablle2013- 1
1.78 + : isac on Isablle2013-1
1.79 :
1.80 - Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013- 1: Test_Isac perfect
1.81 + Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
1.82 User: Walther Neuper <neuper@ist.tugraz.at>
1.83 - Date: 2013- 11- 21 18:12:17 +0100 (2 weeks)
1.84 + Date: 2013-11-21 18:12:17 +0100 (2 weeks)
1.85
1.86 \<close>
1.87
1.88 @@ -443,7 +443,7 @@
1.89 \<close>
1.90 subsubsection \<open>Run tests\<close>
1.91 text \<open>
1.92 - Is standard now; this subsection will be discontinued under Isabelle2013- 1
1.93 + Is standard now; this subsection will be discontinued under Isabelle2013-1
1.94 \<close>
1.95 subsubsection \<open>State of tests\<close>
1.96 text \<open>
1.97 @@ -460,7 +460,7 @@
1.98 :
1.99 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
1.100 User: Walther Neuper <neuper@ist.tugraz.at>
1.101 - Date: 2013-07- 15 08:28:50 +0200 (4 weeks)
1.102 + Date: 2013-07-15 08:28:50 +0200 (4 weeks)
1.103 \<close>
1.104
1.105 subsection \<open>isac on Isabelle2012\<close>
1.106 @@ -484,13 +484,13 @@
1.107 in parallel with evaluation.
1.108
1.109 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
1.110 - yields 69 hits, some of which were already present before Isabelle2002-->2009- 2
1.111 + yields 69 hits, some of which were already present before Isabelle2002-->2009-2
1.112 (i.e. on the old notebook from 2002).
1.113
1.114 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
1.115 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
1.116 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
1.117 - # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009- 2 === , most likely go back to 2002
1.118 + # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
1.119 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
1.120
1.121 Some tests have been re-activated (e.g. error patterns, fill patterns).
1.122 @@ -499,17 +499,17 @@
1.123 text \<open>
1.124 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
1.125 User: Walther Neuper <neuper@ist.tugraz.at>
1.126 - Date: 2013-07- 11 16:58:31 +0200 (4 weeks)
1.127 + Date: 2013-07-11 16:58:31 +0200 (4 weeks)
1.128 :
1.129 : isac on Isablle2012
1.130 :
1.131 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
1.132 User: Walther Neuper <neuper@ist.tugraz.at>
1.133 - Date: 2012-09- 24 18:35:13 +0200 (8 months)
1.134 + Date: 2012-09-24 18:35:13 +0200 (8 months)
1.135 ------------------------------------------------------------------------------
1.136 Changeset: 48756 (7443906996a8) merged
1.137 User: Walther Neuper <neuper@ist.tugraz.at>
1.138 - Date: 2012-09- 24 18:15:49 +0200 (8 months)
1.139 + Date: 2012-09-24 18:15:49 +0200 (8 months)
1.140 \<close>
1.141
1.142 subsection \<open>isac on Isabelle2011\<close>
1.143 @@ -547,7 +547,7 @@
1.144
1.145 The list below records TODOs while producing an ISAC kernel for
1.146 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
1.147 - (so to be resumed with Isabelle2013- 1):
1.148 + (so to be resumed with Isabelle2013-1):
1.149 ############## WNxxxxxx.TODO can be found in sources ##############
1.150 --------------------------------------------------------------------------------
1.151 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
1.152 @@ -569,7 +569,7 @@
1.153 --------------------------------------------------------------------------------
1.154 WN120317.TODO changeset 977788dfed26 dropped rateq:
1.155 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
1.156 - # test --- solve (1/x = 5, x) by me --- and --- x / (x \<up> 2 - 6 * x + 9) - ...:
1.157 + # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
1.158 investigation Check_elementwise stopped due to too much effort finding out,
1.159 why Check_elementwise worked in 2002 in spite of the error.
1.160 --------------------------------------------------------------------------------
1.161 @@ -583,11 +583,11 @@
1.162 --------------------------------------------------------------------------------
1.163 WN120320.TODO check-improve rlsthmsNOTisac:
1.164 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
1.165 - DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09- 2.sml .. Isac.thy
1.166 + DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
1.167 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
1.168 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
1.169 --------------------------------------------------------------------------------
1.170 - WN120320.TODO rlsthmsNOTisac: replace twice thms \<up>
1.171 + WN120320.TODO rlsthmsNOTisac: replace twice thms ^
1.172 --------------------------------------------------------------------------------
1.173 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
1.174 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
1.175 @@ -692,18 +692,18 @@
1.176 ------------------------------------------------------------------------------
1.177 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
1.178 User: Walther Neuper <neuper@ist.tugraz.at>
1.179 - Date: 2012-09- 24 16:39:30 +0200 (8 months)
1.180 + Date: 2012-09-24 16:39:30 +0200 (8 months)
1.181 :
1.182 : isac on Isablle2011
1.183 :
1.184 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
1.185 Branch: decompose-isar
1.186 User: Walther Neuper <neuper@ist.tugraz.at>
1.187 - Date: 2011-02- 25 13:04:56 +0100 (2011-02- 25)
1.188 + Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
1.189 ------------------------------------------------------------------------------
1.190 \<close>
1.191
1.192 -subsection \<open>isac on Isabelle2009- 2\<close>
1.193 +subsection \<open>isac on Isabelle2009-2\<close>
1.194 subsubsection \<open>Summary of development\<close>
1.195 text \<open>
1.196 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
1.197 @@ -716,14 +716,14 @@
1.198 WN131021 this is broken by installation of Isabelle2011/12/13,
1.199 because all these write their binaries to ~/.isabelle/heaps/..
1.200
1.201 - $ cd /usr/local/isabisac09- 2/
1.202 + $ cd /usr/local/isabisac09-2/
1.203 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
1.204 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
1.205 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
1.206 \<close>
1.207 subsubsection \<open>State of tests\<close>
1.208 text \<open>
1.209 - Most tests are broken by the update from Isabelle2002 to Isabelle2009- 2.
1.210 + Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
1.211 \<close>
1.212 subsubsection \<open>Changesets of begin and end\<close>
1.213 text \<open>
1.214 @@ -734,12 +734,12 @@
1.215 User: Marco Steger <m.steger@student.tugraz.at>
1.216 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
1.217 :
1.218 - : isac on Isablle2009- 2
1.219 + : isac on Isablle2009-2
1.220 :
1.221 - Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009- 2
1.222 - Branch: isac-from-Isabelle2009- 2
1.223 + Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
1.224 + Branch: isac-from-Isabelle2009-2
1.225 User: Walther Neuper <neuper@ist.tugraz.at>
1.226 - Date: 2010-07- 21 09:59:35 +0200 (2010-07- 21)
1.227 + Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
1.228 ------------------------------------------------------------------------------
1.229 \<close>
1.230