wenzelm [Tue, 22 May 2012 19:02:17 +0200] rev 48900
Added tag Isabelle2012 for changeset 21c42b095c84
Walther Neuper <neuper@ist.tugraz.at> [Sun, 14 Jul 2013 14:13:44 +0200] rev 48899
tuned
Walther Neuper <neuper@ist.tugraz.at> [Sun, 14 Jul 2013 09:58:28 +0200] rev 48898
--- prepared isac for being fetched into Isabelle2013's repository
deleted files
# which are already present in Isabelle2013 (which is ready for run)
i.e. Admin, bin, lib
# which are not any more in Isabelle2013: doc-src/
but doc-src/isac/ has been retained.
Walther Neuper <neuper@ist.tugraz.at> [Fri, 12 Jul 2013 06:39:55 +0200] rev 48897
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 11 Jul 2013 16:59:05 +0200] rev 48896
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 11 Jul 2013 16:58:31 +0200] rev 48895
end of improving tests for isac on Isabelle2012
improvements:
# reactivated tests for error patterns, fill patterns
# reasons for outcommented test are given as much as possible,
see subsubsection {* State of tests *} in Test_Isac.thy
# detailed "Plans for updating isac from Isabelle2011 to Isabelle2012 and Isabelle2013"
in Build_Thydata.thy
remaining deficiencies:
# Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
yields 69 hits, some of which were already present before Isabelle2002-->2009-2
# many tests are still outcommented; reactivation would require comparison
with isac on Isabelle2002 on an old notebook in many cases.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 30 Jun 2013 17:27:34 +0200] rev 48894
Test_Isac.thy without errors on Isabelle2012, calchead.sml:
WN1130630 THE maximum example WORKS IN isabisac09-2;
MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt in 2010.
Some tests have been broken much earlier,
see test/../calchead.sml "inhibit exn 010830". *)
Walther Neuper <neuper@ist.tugraz.at> [Fri, 21 Jun 2013 17:53:46 +0200] rev 48893
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 21 Jun 2013 17:49:24 +0200] rev 48892
Test_Isac.thy without errors on Isabelle2012, rewtools.sml:
rewtools.sml shows that isac's Context have been broken at Isabelle2009-2 --> 2011.
Walther Neuper <neuper@ist.tugraz.at> [Fri, 21 Jun 2013 11:19:18 +0200] rev 48891
Test_Isac.thy without errors on Isabelle2012, intermediate
intermediate, because there are still some other outcommented tests,
which have been outcommented at transition Isabelle2009-2 --> 11.
The respective files are marked in Test_Isac.thy,
while the files with full tests have not comment (*part*) etc. in Test_Isac.thy.