neuper@52065: (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) neuper@41943: Author: Walther Neuper 101001 neuper@41943: (c) copyright due to lincense terms. neuper@41943: neuper@52065: isac tests neuper@52065: in ~~/test/Tools/isac are structured according neuper@52065: to ~~/src/Tools/isac neuper@52065: Additional tests are in neuper@52065: ~~/test/Tools/isac/ADDTESTS neuper@52065: ~~/test/Tools/isac/Minisubpbl neuper@52065: neuper@52065: $ cd /usr/local/isabisac/ neuper@52065: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & neuper@41943: *) neuper@41943: neuper@52073: (*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: neuper@52073: Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?*) neuper@52073: neuper@52067: theory Test_Isac imports Isac neuper@41980: "ADDTESTS/Ctxt" neuper@42048: "ADDTESTS/test-depend/Build_Test" neuper@42023: "ADDTESTS/All_Ctxt" neuper@42179: "ADDTESTS/course/phst11/T1_Basics" neuper@42092: "ADDTESTS/course/phst11/T2_Rewriting" neuper@42179: "ADDTESTS/course/phst11/T3_MathEngine" neuper@52065: "ADDTESTS/file-depend/BuildC_Test" neuper@42280: "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" neuper@52073: "~~/test/Pure/Isar/Test_Parsers" neuper@52073: (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*) neuper@52073: "~~/test/Pure/Isar/Test_Parse_Term" neuper@52073: "~~/test/HOL/Library/Test_Polynomial" neuper@52073: neuper@52073: "~~/src/Tools/isac/Knowledge/GCD_Poly" (*not imported by Isac.thy*) neuper@52073: "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) neuper@42387: neuper@52079: (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) neuper@52079: (* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *) neuper@52079: (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) neuper@52079: neuper@41943: begin neuper@48895: section {* test ML Code of isac *} neuper@48895: ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "library.sml" neuper@52065: ML_file "calcelems.sml" neuper@52065: ML_file "ProgLang/termC.sml" neuper@52065: ML_file "ProgLang/calculate.sml" neuper@52065: ML_file "ProgLang/rewrite.sml" neuper@52065: (*ML_file "ProgLang/listC.sml" 2002*) neuper@52065: ML_file "ProgLang/scrtools.sml" neuper@52065: ML_file "ProgLang/tools.sml" neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@41986: ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "Minisubpbl/000-comments.sml" neuper@52065: ML_file "Minisubpbl/100-init-rootpbl.sml" neuper@52065: ML_file "Minisubpbl/150-add-given.sml" neuper@52065: ML_file "Minisubpbl/200-start-method.sml" neuper@52065: ML_file "Minisubpbl/300-init-subpbl.sml" neuper@52065: ML_file "Minisubpbl/400-start-meth-subpbl.sml" neuper@52065: ML_file "Minisubpbl/490-nxt-Check_Postcond.sml" neuper@52065: ML_file "Minisubpbl/500-met-sub-to-root.sml" neuper@52065: ML_file "Minisubpbl/530-error-Check_Elementwise.sml" neuper@52065: ML_file "Minisubpbl/600-postcond.sml" akargl@42188: ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "Interpret/mstools.sml" neuper@52065: ML_file "Interpret/ctree.sml" (*!...!see(25)*) neuper@52065: ML_file "Interpret/ptyps.sml" neuper@48891: ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *} neuper@48895: (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*) neuper@52065: ML_file "Interpret/generate.sml" neuper@48895: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: neuper@48895: ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) neuper@52065: ML_file "Interpret/calchead.sml" neuper@52065: ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *) neuper@52065: ML_file "Interpret/rewtools.sml" (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*) neuper@52065: ML_file "Interpret/script.sml" neuper@52065: ML_file "Interpret/solve.sml" neuper@52065: ML_file "Interpret/inform.sml" neuper@48895: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: neuper@48895: ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) neuper@52065: ML_file "Interpret/mathengine.sml" (*!part.*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "xmlsrc/mathml.sml" (*part.*) neuper@52065: ML_file "xmlsrc/datatypes.sml" (*TODO/part.*) neuper@52065: ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*) neuper@52065: (*ML_file "xmlsrc/thy-hierarchy.sml" TODO after 2009-2/part | Isabelle2012-->13 !thehier! *) neuper@48895: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: neuper@48895: val it = "----------- ### thes2file ... Exception- Match raised -----------": string neuper@48889: : neuper@48889: val it = "~~~~~ fun thes2file, args:": string neuper@48889: val p = "../../tmp/": path neuper@48889: val it = (): unit neuper@48889: exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml") neuper@48889: ...CONCERNED WITH thehier neuper@48889: *) neuper@52065: ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "Frontend/messages.sml" neuper@52065: ML_file "Frontend/states.sml" neuper@52065: ML_file "Frontend/interface.sml" neuper@48895: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: neuper@48895: ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) neuper@52065: ML_file "print_exn_G.sml" neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@48895: ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "Knowledge/delete.sml" neuper@52065: ML_file "Knowledge/descript.sml" neuper@52065: ML_file "Knowledge/atools.sml" neuper@52065: ML_file "Knowledge/simplify.sml" neuper@52065: ML_file "Knowledge/poly.sml" neuper@48884: (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0 neuper@52065: ML_file "Knowledge/gcd_poly.sml" (*type error 'nth' etc*) neuper@52065: ML_file "Knowledge/gcd_poly_winkler.sml"*) neuper@52065: (*ML_file "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *) neuper@52065: ML_file "Knowledge/equation.sml" neuper@52065: ML_file "Knowledge/root.sml" neuper@52065: ML_file "Knowledge/lineq.sml" neuper@52065: (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) neuper@52065: ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) neuper@52065: ML_file "Knowledge/rootrat.sml" neuper@52065: ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) neuper@52065: ML_file "Knowledge/partial_fractions.sml" neuper@52065: ML_file "Knowledge/polyeq.sml" neuper@52065: (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) neuper@52065: ML_file "Knowledge/calculus.sml" neuper@52065: ML_file "Knowledge/trig.sml" neuper@52065: (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) neuper@52065: ML_file "Knowledge/diff.sml" neuper@52065: ML_file "Knowledge/integrate.sml" neuper@52065: ML_file "Knowledge/eqsystem.sml" neuper@52065: ML_file "Knowledge/test.sml" neuper@52065: ML_file "Knowledge/polyminus.sml" neuper@52065: ML_file "Knowledge/vect.sml" neuper@52065: ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *) neuper@52065: ML_file "Knowledge/biegelinie.sml" neuper@52065: ML_file "Knowledge/algein.sml" neuper@52065: ML_file "Knowledge/diophanteq.sml" neuper@52065: ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" neuper@52073: ML_file "Knowledge/gcd_poly_ml.sml" neuper@52073: ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) neuper@52065: ML_file "Knowledge/isac.sml" neuper@52065: ML_file "Knowledge/build_thydata.sml" neuper@48895: ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: neuper@48895: section {* history of tests *} neuper@48895: text {* neuper@48895: Systematic regression tests have been introduced to isac development in 2003. neuper@48895: Sanity of the regression test suffered from updates following Isabelle development, neuper@48895: which mostly exceeded the resources available in isac's development. neuper@48895: neuper@48895: The survey below shall support to efficiently use the tests for isac neuper@48895: on different Isabelle versions. Conclusion in most cases will be: neuper@48895: neuper@48895: !!! Use most recent tests or go back to the old notebook neuper@48895: with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2013 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@48895: *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@48895: text {* neuper@52079: TODO neuper@52079: : neuper@52079: : isac on Isablle2013 neuper@52079: : neuper@52079: Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013 neuper@52079: User: Walther Neuper neuper@52079: Date: 2013-07-15 08:28:50 +0200 (4 weeks) neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2012 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: isac on Isabelle2012 is considered just a transitional stage neuper@48895: within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; neuper@48895: For considerations on the transition see neuper@48895: ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..". neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@48895: $ cd /usr/local/isabisac12/ neuper@48895: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy neuper@48895: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy neuper@48895: *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: At least the tests from isac on Isabelle2011 run again. neuper@48895: However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling neuper@48895: in parallel with evaluation. neuper@48895: neuper@48895: Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant) neuper@48895: yields 69 hits, some of which were already present before Isabelle2002-->2009-2 neuper@48895: (i.e. on the old notebook from 2002). neuper@48895: neuper@48895: Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin: neuper@48895: # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy neuper@48895: # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002 neuper@48895: # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002 neuper@48895: Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml. neuper@48895: neuper@48895: Some tests have been re-activated (e.g. error patterns, fill patterns). neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@52079: text {* neuper@52079: Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012 neuper@52079: User: Walther Neuper neuper@52079: Date: 2013-07-11 16:58:31 +0200 (4 weeks) neuper@48895: : neuper@48895: : isac on Isablle2012 neuper@48895: : neuper@48895: Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012 neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-09-24 18:35:13 +0200 (8 months) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: Changeset: 48756 (7443906996a8) merged neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-09-24 18:15:49 +0200 (8 months) neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2011 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: isac's mathematics engine has been extended by two developments: neuper@48895: (1) Isabelle's contexts were introduced by Mathias Lehnfeld neuper@48895: (2) "error patterns" were introduced by Gabriella Daroczy neuper@48895: Regressions tests have been added for both. neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@48895: $ cd /usr/local/isabisac11/ neuper@48895: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy neuper@48895: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy neuper@48895: *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*) neuper@48895: and sometimes give reasons for failing tests. neuper@48895: (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable neuper@48895: work, some of which couldn't be revised (and renamed) by WN and thus survived some time. neuper@48895: neuper@48895: Tests with functions decomposed for single-stepping are marked with neuper@48895: "~~~~~ fun , args:"; val neuper@48895: neuper@48895: The most signification tests (in particular Frontend/interface.sml) run, neuper@48895: however, many "error in kernel" are not caught by an exception. neuper@48895: ------------------------------------------------------------------------------ neuper@48895: After the changeset below Test_Isac worked with check_unsynchronized_ref (): neuper@48895: ------------------------------------------------------------------------------ neuper@48895: Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-08-06 10:38:11 +0200 (11 months) neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@48895: text {* neuper@48895: isac development was done between these changesets: neuper@48895: ------------------------------------------------------------------------------ neuper@48895: Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-09-24 16:39:30 +0200 (8 months) neuper@48895: : neuper@48895: : isac on Isablle2011 neuper@48895: : neuper@48895: Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011 neuper@48895: Branch: decompose-isar neuper@48895: User: Walther Neuper neuper@48895: Date: 2011-02-25 13:04:56 +0100 (2011-02-25) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2009-2 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg. neuper@48895: The update was painful (bridging 7 years of Isabelle development) and cut short neuper@48895: due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and neuper@48895: going on to Isabelle2011 although most of the tests did not run. neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@48895: $ cd /usr/local/isabisac09-2/ neuper@48895: $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy neuper@48895: $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy neuper@48895: NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!! neuper@48895: *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: Most tests are broken by the update from Isabelle2002 to Isabelle2009-2. neuper@48895: If really necessary, go back to the old notebook with Isabelle2002. neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@48895: text {* neuper@48895: isac development was done between these changesets: neuper@48895: ------------------------------------------------------------------------------ neuper@48895: Changeset: 38115 (940a5feea094) Little improvements of isac-plugin neuper@48895: Branch: decompose-isar neuper@48895: User: Marco Steger neuper@48895: Date: 2011-02-06 18:30:28 +0100 (2011-02-06) neuper@48895: : neuper@48895: : isac on Isablle2009-2 neuper@48895: : neuper@48895: Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 neuper@48895: Branch: isac-from-Isabelle2009-2 neuper@48895: User: Walther Neuper neuper@48895: Date: 2010-07-21 09:59:35 +0200 (2010-07-21) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2002 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern") neuper@48895: of isac's mathematics engine has been implemented. neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: All tests work on an old notebook (the right PolyML coudn't be upgraded to more neuper@48895: recent Linux versions) neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@48895: text {* neuper@48895: Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS; neuper@48895: see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial. neuper@48895: *} neuper@48895: neuper@41943: end neuper@52065: (*========== inhibit exn 130719 Isabelle2013 =================================== neuper@52065: ============ inhibit exn 130719 Isabelle2013 =================================*) neuper@41943: neuper@41943: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@48895: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@41975: