Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Test_Isac.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 14 Aug 2013 14:32:18 +0200
changeset 52079 0e17ac93bbed
parent 52073 f709e6ab4e09
child 52088 a05261fc089e
permissions -rwxr-xr-x
tuned 
     1 (* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)

     2    Author: Walther Neuper 101001

     3    (c) copyright due to lincense terms.

     4 

     5    isac tests 

     6      in ~~/test/Tools/isac are structured according 

     7      to ~~/src/Tools/isac

     8    Additional tests are in

     9      ~~/test/Tools/isac/ADDTESTS

    10      ~~/test/Tools/isac/Minisubpbl

    11 

    12 $ cd /usr/local/isabisac/

    13 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &

    14 *)

    15 

    16 (*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: 

    17   Tracing paused.  Stop, or continue with next 100, 1000, 10000 messages?*)

    18 

    19 theory Test_Isac imports Isac

    20   "ADDTESTS/Ctxt"

    21   "ADDTESTS/test-depend/Build_Test"

    22   "ADDTESTS/All_Ctxt"

    23   "ADDTESTS/course/phst11/T1_Basics"

    24   "ADDTESTS/course/phst11/T2_Rewriting"

    25   "ADDTESTS/course/phst11/T3_MathEngine"

    26   "ADDTESTS/file-depend/BuildC_Test"

    27   "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"

    28   "~~/test/Pure/Isar/Test_Parsers"

    29 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)

    30   "~~/test/Pure/Isar/Test_Parse_Term"

    31   "~~/test/HOL/Library/Test_Polynomial"

    32 

    33   "~~/src/Tools/isac/Knowledge/GCD_Poly"    (*not imported by Isac.thy*)

    34   "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)

    35 

    36 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)

    37 (* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *)

    38 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)

    39 

    40 begin

    41 section {* test ML Code of isac *}

    42   ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}

    43   ML_file          "library.sml"

    44   ML_file          "calcelems.sml"

    45   ML_file "ProgLang/termC.sml"

    46   ML_file "ProgLang/calculate.sml"

    47   ML_file "ProgLang/rewrite.sml"

    48 (*ML_file "ProgLang/listC.sml"            2002*)

    49   ML_file "ProgLang/scrtools.sml"

    50   ML_file "ProgLang/tools.sml"

    51   ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}

    52   ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}

    53   ML_file "Minisubpbl/000-comments.sml"

    54   ML_file "Minisubpbl/100-init-rootpbl.sml"

    55   ML_file "Minisubpbl/150-add-given.sml"

    56   ML_file "Minisubpbl/200-start-method.sml"

    57   ML_file "Minisubpbl/300-init-subpbl.sml"

    58   ML_file "Minisubpbl/400-start-meth-subpbl.sml"

    59   ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"

    60   ML_file "Minisubpbl/500-met-sub-to-root.sml"

    61   ML_file "Minisubpbl/530-error-Check_Elementwise.sml"

    62   ML_file "Minisubpbl/600-postcond.sml"

    63   ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

    64   ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}

    65   ML_file "Interpret/mstools.sml"

    66   ML_file "Interpret/ctree.sml"         (*!...!see(25)*)

    67   ML_file "Interpret/ptyps.sml"

    68   ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}

    69 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)

    70   ML_file "Interpret/generate.sml"

    71 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

    72   ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

    73   ML_file "Interpret/calchead.sml"

    74   ML_file "Interpret/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"                          *)

    75   ML_file "Interpret/rewtools.sml"      (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)

    76   ML_file "Interpret/script.sml"

    77   ML_file "Interpret/solve.sml"

    78   ML_file "Interpret/inform.sml"

    79 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

    80   ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

    81   ML_file "Interpret/mathengine.sml"    (*!part.*)

    82   ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}

    83   ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}

    84   ML_file "xmlsrc/mathml.sml"           (*part.*)

    85   ML_file "xmlsrc/datatypes.sml"        (*TODO/part.*)

    86   ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)

    87 (*ML_file "xmlsrc/thy-hierarchy.sml"      TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)

    88 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

    89 val it = "----------- ### thes2file ... Exception- Match raised -----------": string

    90 :

    91 val it = "~~~~~ fun thes2file, args:": string

    92 val p = "../../tmp/": path

    93 val it = (): unit

    94  exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")

    95                                                  ...CONCERNED WITH thehier

    96 *)

    97   ML_file "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)

    98   ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

    99   ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}

   100   ML_file "Frontend/messages.sml"

   101   ML_file "Frontend/states.sml"

   102   ML_file "Frontend/interface.sml"

   103 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:

   104   ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)

   105   ML_file          "print_exn_G.sml"

   106   ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}

   107   ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}

   108   ML_file "Knowledge/delete.sml"

   109   ML_file "Knowledge/descript.sml"

   110   ML_file "Knowledge/atools.sml"

   111   ML_file "Knowledge/simplify.sml"

   112   ML_file "Knowledge/poly.sml"

   113 (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0

   114   ML_file "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)

   115   ML_file "Knowledge/gcd_poly_winkler.sml"*)

   116 (*ML_file "Knowledge/rational.sml"  WN120317.TODO postponed to joint work with dmeindl *)

   117   ML_file "Knowledge/equation.sml"

   118   ML_file "Knowledge/root.sml"

   119   ML_file "Knowledge/lineq.sml"

   120 (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)

   121   ML_file "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)

   122   ML_file "Knowledge/rootrat.sml"

   123   ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)

   124   ML_file "Knowledge/partial_fractions.sml"

   125   ML_file "Knowledge/polyeq.sml"

   126 (*ML_file "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)

   127   ML_file "Knowledge/calculus.sml"

   128   ML_file "Knowledge/trig.sml"

   129 (*ML_file "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 

   130   ML_file "Knowledge/diff.sml"

   131   ML_file "Knowledge/integrate.sml"

   132   ML_file "Knowledge/eqsystem.sml"

   133   ML_file "Knowledge/test.sml"

   134   ML_file "Knowledge/polyminus.sml"

   135   ML_file "Knowledge/vect.sml"

   136   ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)

   137   ML_file "Knowledge/biegelinie.sml"

   138   ML_file "Knowledge/algein.sml"

   139   ML_file "Knowledge/diophanteq.sml"

   140   ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"

   141   ML_file "Knowledge/gcd_poly_ml.sml"

   142   ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)

   143   ML_file "Knowledge/isac.sml"

   144   ML_file "Knowledge/build_thydata.sml"

   145   ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}

   146   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

   147   ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}

   148   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

   149 

   150 section {* history of tests *}

   151 text {*

   152   Systematic regression tests have been introduced to isac development in 2003.

   153   Sanity of the regression test suffered from updates following Isabelle development,

   154   which mostly exceeded the resources available in isac's development.

   155 

   156   The survey below shall support to efficiently use the tests for isac 

   157   on different Isabelle versions. Conclusion in most cases will be: 

   158 

   159   !!! Use most recent tests or go back to the old notebook

   160       with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   161 *}

   162 

   163 subsection {* isac on Isabelle2013 *}

   164 subsubsection {* Summary of development *}

   165 text {*

   166 *}

   167 subsubsection {* Run tests *}

   168 text {*

   169 *}

   170 subsubsection {* State of tests *}

   171 text {*

   172 *}

   173 subsubsection {* Changesets of begin and end *}

   174 text {*

   175   TODO

   176   :

   177   : isac on Isablle2013 

   178   :

   179   Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013

   180   User: Walther Neuper <neuper@ist.tugraz.at>

   181   Date: 2013-07-15 08:28:50 +0200 (4 weeks)

   182 *}

   183 

   184 subsection {* isac on Isabelle2012 *}

   185 subsubsection {* Summary of development *}

   186 text {*

   187   isac on Isabelle2012 is considered just a transitional stage

   188   within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;

   189   For considerations on the transition see 

   190   ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".

   191 *}

   192 subsubsection {* Run tests *}

   193 text {*

   194 $ cd /usr/local/isabisac12/

   195 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy

   196 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy

   197 *}

   198 subsubsection {* State of tests *}

   199 text {*

   200   At least the tests from isac on Isabelle2011 run again.

   201   However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling 

   202   in parallel with evaluation.

   203 

   204   Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)

   205   yields 69 hits, some of which were already present before Isabelle2002-->2009-2

   206   (i.e. on the old notebook from 2002).

   207 

   208   Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:

   209   # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy

   210   # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002

   211   # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002

   212   Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.

   213 

   214   Some tests have been re-activated (e.g. error patterns, fill patterns).

   215 *}

   216 subsubsection {* Changesets of begin and end *}

   217 text {*  

   218   Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012

   219   User: Walther Neuper <neuper@ist.tugraz.at>

   220   Date: 2013-07-11 16:58:31 +0200 (4 weeks)

   221   :

   222   : isac on Isablle2012 

   223   :

   224   Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012

   225   User: Walther Neuper <neuper@ist.tugraz.at>

   226   Date: 2012-09-24 18:35:13 +0200 (8 months)

   227   ------------------------------------------------------------------------------

   228   Changeset: 48756 (7443906996a8) merged

   229   User: Walther Neuper <neuper@ist.tugraz.at>

   230   Date: 2012-09-24 18:15:49 +0200 (8 months)

   231 *}

   232 

   233 subsection {* isac on Isabelle2011 *}

   234 subsubsection {* Summary of development *}

   235 text {*

   236   isac's mathematics engine has been extended by two developments:

   237   (1) Isabelle's contexts were introduced by Mathias Lehnfeld

   238   (2) "error patterns" were introduced by Gabriella Daroczy

   239   Regressions tests have been added for both.

   240 *}

   241 subsubsection {* Run tests *}

   242 text {*

   243   $ cd /usr/local/isabisac11/

   244   $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy

   245   $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy

   246 *}

   247 subsubsection {* State of tests *}

   248 text {* 

   249   Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*) 

   250   and sometimes give reasons for failing tests.

   251   (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable

   252   work, some of which couldn't be revised (and renamed) by WN and thus survived some time.

   253 

   254   Tests with functions decomposed for single-stepping are marked with

   255   "~~~~~ fun , args:"; val 

   256 

   257   The most signification tests (in particular Frontend/interface.sml) run,

   258   however, many "error in kernel" are not caught by an exception.

   259   ------------------------------------------------------------------------------

   260   After the changeset below Test_Isac worked with check_unsynchronized_ref ():

   261   ------------------------------------------------------------------------------

   262   Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref

   263   User: Walther Neuper <neuper@ist.tugraz.at>

   264   Date: 2012-08-06 10:38:11 +0200 (11 months)

   265 *}

   266 subsubsection {* Changesets of begin and end *}

   267 text {*

   268   isac development was done between these changesets:

   269   ------------------------------------------------------------------------------

   270   Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files

   271   User: Walther Neuper <neuper@ist.tugraz.at>

   272   Date: 2012-09-24 16:39:30 +0200 (8 months)

   273   :

   274   : isac on Isablle2011

   275   :

   276   Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011

   277   Branch: decompose-isar 

   278   User: Walther Neuper <neuper@ist.tugraz.at>

   279   Date: 2011-02-25 13:04:56 +0100 (2011-02-25)

   280   ------------------------------------------------------------------------------

   281 *}

   282 

   283 subsection {* isac on Isabelle2009-2 *}

   284 subsubsection {* Summary of development *}

   285 text {*

   286   In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.

   287   The update was painful (bridging 7 years of Isabelle development) and cut short 

   288   due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and

   289   going on to Isabelle2011 although most of the tests did not run.

   290 *}

   291 subsubsection {* Run tests *}

   292 text {*

   293   $ cd /usr/local/isabisac09-2/

   294   $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy

   295   $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy

   296   NOT THE RIGHT VERSION.....    test/Tools/isac/Test_Isac.thy !!!

   297 *}

   298 subsubsection {* State of tests *}

   299 text {* 

   300   Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.

   301   If really necessary, go back to the old notebook with Isabelle2002.

   302 *}

   303 subsubsection {* Changesets of begin and end *}

   304 text {*

   305   isac development was done between these changesets:

   306   ------------------------------------------------------------------------------

   307   Changeset: 38115 (940a5feea094) Little improvements of isac-plugin

   308   Branch: decompose-isar 

   309   User: Marco Steger <m.steger@student.tugraz.at>

   310   Date: 2011-02-06 18:30:28 +0100 (2011-02-06)

   311   :

   312   : isac on Isablle2009-2

   313   :

   314   Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2

   315   Branch: isac-from-Isabelle2009-2 

   316   User: Walther Neuper <neuper@ist.tugraz.at>

   317   Date: 2010-07-21 09:59:35 +0200 (2010-07-21)

   318   ------------------------------------------------------------------------------

   319 *}

   320 

   321 subsection {* isac on Isabelle2002 *}

   322 subsubsection {* Summary of development *}

   323 text {*

   324   From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")

   325   of isac's mathematics engine has been implemented.

   326 *}

   327 subsubsection {* Run tests *}

   328 subsubsection {* State of tests *}

   329 text {* 

   330   All tests work on an old notebook (the right PolyML coudn't be upgraded to more

   331   recent Linux versions)

   332 *}

   333 subsubsection {* Changesets of begin and end *}

   334 text {*

   335   Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;

   336   see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.

   337 *}

   338 

   339 end

   340 (*========== inhibit exn 130719 Isabelle2013 ===================================

   341 ============ inhibit exn 130719 Isabelle2013 =================================*)

   342 

   343 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   344   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   345
wneuper/isa