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>
Mon, 26 Aug 2013 11:20:41 +0200
changeset 52090 9642feb9e96b
parent 52089 7a740eedefc0
child 52101 c3f399ce32af
permissions -rwxr-xr-x
Test_Isac doesn't work anymore

after successful build of session Isac
./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
# launches jEdit
# loads the required theories
# once highlights the additional theories required
# and then doesn't start evaluation with 10 minutes.

next trial will delete the old Unsynchronized.ref in Rational.thy
which are not necessary anymore. 
     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" lost at 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 (* !!!!! with this changeset evaluation doen't start < 7min; UG is busy ! *)

    40 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)

    41 

    42 begin

    43 section {* test ML Code of isac *}

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

    45   ML_file          "library.sml"

    46   ML_file          "calcelems.sml"

    47   ML_file "ProgLang/termC.sml"

    48   ML_file "ProgLang/calculate.sml"

    49   ML_file "ProgLang/rewrite.sml"

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

    51   ML_file "ProgLang/scrtools.sml"

    52   ML_file "ProgLang/tools.sml"

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

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

    55   ML_file "Minisubpbl/000-comments.sml"

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

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

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

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

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

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

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

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

    64   ML_file "Minisubpbl/600-postcond.sml"

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

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

    67   ML_file "Interpret/mstools.sml"

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

    69   ML_file "Interpret/ptyps.sml"

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

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

    72   ML_file "Interpret/generate.sml"

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

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

    75   ML_file "Interpret/calchead.sml"

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

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

    78   ML_file "Interpret/script.sml"

    79   ML_file "Interpret/solve.sml"

    80   ML_file "Interpret/inform.sml"

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

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

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

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

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

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

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

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

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

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

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

    92 :

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

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

    95 val it = (): unit

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

    97                                                  ...CONCERNED WITH thehier

    98 *)

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

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

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

   102   ML_file "Frontend/messages.sml"

   103   ML_file "Frontend/states.sml"

   104   ML_file "Frontend/interface.sml"

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

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

   107   ML_file          "print_exn_G.sml"

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

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

   110   ML_file "Knowledge/delete.sml"

   111   ML_file "Knowledge/descript.sml"

   112   ML_file "Knowledge/atools.sml"

   113   ML_file "Knowledge/simplify.sml"

   114   ML_file "Knowledge/poly.sml"

   115   ML_file "Knowledge/gcd_poly_ml.sml"

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

   117   ML_file "Knowledge/rational.sml"

   118   ML_file "Knowledge/equation.sml"

   119   ML_file "Knowledge/root.sml"

   120   ML_file "Knowledge/lineq.sml"

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

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

   123   ML_file "Knowledge/rootrat.sml"

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

   125   ML_file "Knowledge/partial_fractions.sml"

   126 (*ML_file "Knowledge/polyeq.sml"   -----------------works if cut into parts !!!!!!!!!!!*)

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

   128   ML_file "Knowledge/calculus.sml"

   129   ML_file "Knowledge/trig.sml"

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

   131   ML_file "Knowledge/diff.sml"

   132   ML_file "Knowledge/integrate.sml"

   133   ML_file "Knowledge/eqsystem.sml"

   134   ML_file "Knowledge/test.sml"

   135   ML_file "Knowledge/polyminus.sml"

   136   ML_file "Knowledge/vect.sml"

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

   138   ML_file "Knowledge/biegelinie.sml"

   139   ML_file "Knowledge/algein.sml"

   140   ML_file "Knowledge/diophanteq.sml"

   141   ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"

   142   ML_file "Knowledge/isac.sml"

   143   ML_file "Knowledge/build_thydata.sml"

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

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

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

   147   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

   148 

   149 section {* history of tests *}

   150 text {*

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

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

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

   154 

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

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

   157 

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

   159       with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   160 *}

   161 

   162 subsection {* isac on Isabelle2013 *}

   163 subsubsection {* Summary of development *}

   164 text {*

   165 *}

   166 subsubsection {* Run tests *}

   167 text {*

   168 *}

   169 subsubsection {* State of tests *}

   170 text {*

   171 *}

   172 subsubsection {* Changesets of begin and end *}

   173 text {*

   174   TODO

   175   :

   176   : isac on Isablle2013 

   177   :

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

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

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

   181 *}

   182 

   183 subsection {* isac on Isabelle2012 *}

   184 subsubsection {* Summary of development *}

   185 text {*

   186   isac on Isabelle2012 is considered just a transitional stage

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

   188   For considerations on the transition see 

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

   190 *}

   191 subsubsection {* Run tests *}

   192 text {*

   193 $ cd /usr/local/isabisac12/

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

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

   196 *}

   197 subsubsection {* State of tests *}

   198 text {*

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

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

   201   in parallel with evaluation.

   202 

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

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

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

   206 

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

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

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

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

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

   212 

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

   214 *}

   215 subsubsection {* Changesets of begin and end *}

   216 text {*  

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

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

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

   220   :

   221   : isac on Isablle2012 

   222   :

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

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

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

   226   ------------------------------------------------------------------------------

   227   Changeset: 48756 (7443906996a8) merged

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

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

   230 *}

   231 

   232 subsection {* isac on Isabelle2011 *}

   233 subsubsection {* Summary of development *}

   234 text {*

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

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

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

   238   Regressions tests have been added for both.

   239 *}

   240 subsubsection {* Run tests *}

   241 text {*

   242   $ cd /usr/local/isabisac11/

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

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

   245 *}

   246 subsubsection {* State of tests *}

   247 text {* 

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

   249   and sometimes give reasons for failing tests.

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

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

   252 

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

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

   255 

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

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

   258   ------------------------------------------------------------------------------

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

   260   ------------------------------------------------------------------------------

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

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

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

   264 *}

   265 subsubsection {* Changesets of begin and end *}

   266 text {*

   267   isac development was done between these changesets:

   268   ------------------------------------------------------------------------------

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

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

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

   272   :

   273   : isac on Isablle2011

   274   :

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

   276   Branch: decompose-isar 

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

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

   279   ------------------------------------------------------------------------------

   280 *}

   281 

   282 subsection {* isac on Isabelle2009-2 *}

   283 subsubsection {* Summary of development *}

   284 text {*

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

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

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

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

   289 *}

   290 subsubsection {* Run tests *}

   291 text {*

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

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

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

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

   296 *}

   297 subsubsection {* State of tests *}

   298 text {* 

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

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

   301 *}

   302 subsubsection {* Changesets of begin and end *}

   303 text {*

   304   isac development was done between these changesets:

   305   ------------------------------------------------------------------------------

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

   307   Branch: decompose-isar 

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

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

   310   :

   311   : isac on Isablle2009-2

   312   :

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

   314   Branch: isac-from-Isabelle2009-2 

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

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

   317   ------------------------------------------------------------------------------

   318 *}

   319 

   320 subsection {* isac on Isabelle2002 *}

   321 subsubsection {* Summary of development *}

   322 text {*

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

   324   of isac's mathematics engine has been implemented.

   325 *}

   326 subsubsection {* Run tests *}

   327 subsubsection {* State of tests *}

   328 text {* 

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

   330   recent Linux versions)

   331 *}

   332 subsubsection {* Changesets of begin and end *}

   333 text {*

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

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

   336 *}

   337 

   338 end

   339 (*========== inhibit exn 130719 Isabelle2013 ===================================

   340 ============ inhibit exn 130719 Isabelle2013 =================================*)

   341 

   342 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   343   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   344
wneuper/isa