wneuper/isa: test/Tools/isac/Test_Isac

     1 (* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)

     2    Author: Walther Neuper 101001

     3    (c) copyright due to license terms.

     5    Isac's tests are organised parallel to sources:

     6      $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC

     7    plus

     8      $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS

     9      $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality

    11 Note, that only the first error in a file is shown here.

    12 *)

    14 section \<open>Notes on running tests\<close>

    15 subsection \<open>Switch between running tests and updating code\<close>

    16 text \<open>

    17   Isac encapsulates code as much as possible in structures without open.

    18   This policy conflicts with those tests, which go into functions to details

    19   not declared in the signatures.

    20 \<close>

    21 subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>

    22 text \<open>

    23   Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")

    24   if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).

    25   This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.

    26   A model is in the repository at ~~/etc/preferences.

    27   These preferences have drawbacks, however:

    28   * they claim more memory such that Isabelle instances canNOT run in parallel.

    29   * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.

    31   So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.

    32   From time to time full testing in Test_Isac.thy is recommended. For that purpose

    33   * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.

    35 \\******************* don't forget to re-set defaults BEFORE updating code *******************//

    37     Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use

    38     ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &

    39 \<close>

    41 section \<open>Run the tests\<close>

    42 text \<open>

    43 * say "OK" to the popup asking for theories to be loaded

    44 * watch the <Theories> window for errors in the "imports" below

    45 \<close>

    47 theory Test_Isac_Short

    48   imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)

    49   (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one

    50      and find out, which ML_file or *.thy causes an error (might be ONLY one).

    51      Also backup files (#* ) recognised by jEdit cause this trouble                    *)

    52 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)

    53 (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)

    54 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"

    55 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"

    56 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"

    57 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"

    58 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"

    59 (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*)

    60 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"

    61 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"

    62 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"

    63 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"

    64    ADDTESTS/------------------------------------------- see end of tests *)

    65 (*/~~~ these work directly from Pure, but create problems here ..

    66   "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)

    67   "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)

    68   "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)

    69   "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands"            (* Duplicate outer syntax command "ISAC"   *)

    70   "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized"        (* re-defines / breaks structures      !!! *)

    71   \~~~ .. these work independently, but create problems here *)

    72 (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"

    73 (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"

    74 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)

    75   "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

    76   "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)

    77   "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)

    78 (** )

    79 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)

    80 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)

    81 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)

    82 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)

    83 ( **)

    85 begin

    87 declare [[ML_print_depth = 20]]

    89 ML \<open>open ML_System\<close>

    90 ML \<open>

    91   open Kernel;

    92   open Math_Engine;

    93   open Test_Code;              CalcTreeTEST;

    94   open LItool;                 arguments_from_model;

    95   open Sub_Problem;

    96   open Fetch_Tacs;

    97   open Step

    98   open Env;

    99   open LI;                     scan_dn;

   100   open Istate;

   101   open Error_Pattern;

   102   open Error_Pattern_Def;

   103   open Specification;

   104   open Ctree;                  append_problem;

   105   open Pos;

   106   open Program;

   107   open Prog_Tac;

   108   open Tactical;

   109   open Prog_Expr;

   110   open Auto_Prog;              rule2stac;

   111   open Input_Descript;

   112   open Specify;

   113   open Specify;

   114   open Step_Specify;

   115   open Step_Solve;

   116   open Step;

   117   open Solve;                  (* NONE *)

   118   open ContextC;               transfer_asms_from_to;

   119   open Tactic;                 (* NONE *)

   120   open I_Model;

   121   open O_Model;

   122   open P_Model;                (* NONE *)

   123   open Rewrite;

   124   open Eval;                   get_pair;

   125   open TermC;                  atomt;

   126   open Rule;

   127   open Rule_Set;               Sequence;

   128   open Eval_Def

   129   open ThyC

   130   open ThmC_Def

   131   open ThmC

   132   open Rewrite_Ord

   133   open UnparseC

   134 \<close>

   136 ML \<open>

   137 "~~~~~ fun xxx , args:"; val () = ();

   138 "~~~~~ and xxx , args:"; val () = ();

   139 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

   140 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

   141 "xx"

   142 ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)

   143 \<close> ML \<open>

   144 \<close>

   145 ML \<open>

   146 \<close> ML \<open>

   147 \<close> ML \<open>

   148 \<close> ML \<open>

   149 \<close> ML \<open>

   150 \<close> ML \<open>

   151 \<close> ML \<open>

   152 \<close> ML \<open>

   153 \<close> ML \<open>

   154 \<close> ML \<open>

   155 \<close> ML \<open>

   156 \<close>

   158 ML \<open>

   159   KEStore_Elems.set_ref_thy @{theory};

   160   (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);

   161 \<close>

   163 (*---------------------- check test file by testfile -------------------------------------------

   164   ---------------------- check test file by testfile -------------------------------------------*)

   165 section \<open>trials with Isabelle's functions\<close>

   166   ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>

   167   ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"

   168   ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"

   169   ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"

   170   ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"

   171   ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>

   173 section \<open>test ML Code of isac\<close>

   174 subsection \<open>basic code first\<close>

   175   ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>

   176   ML_file "BaseDefinitions/libraryC.sml"

   177   ML_file "BaseDefinitions/rule-def.sml"

   178   ML_file "BaseDefinitions/eval-def.sml"

   179   ML_file "BaseDefinitions/rewrite-order.sml"

   180   ML_file "BaseDefinitions/theoryC.sml"

   181   ML_file "BaseDefinitions/rule.sml"

   182   ML_file "BaseDefinitions/thmC-def.sml"

   183   ML_file "BaseDefinitions/error-fill-def.sml"

   184   ML_file "BaseDefinitions/rule-set.sml"

   185   ML_file "BaseDefinitions/check-unique.sml"

   186 (*called by Know_Store..*)

   187   ML_file "BaseDefinitions/calcelems.sml"

   188   ML_file "BaseDefinitions/termC.sml"

   189   ML_file "BaseDefinitions/substitution.sml"

   190   ML_file "BaseDefinitions/contextC.sml"

   191   ML_file "BaseDefinitions/environment.sml"

   192 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)

   193 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

   194   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

   196   ML_file "ProgLang/calculate.sml"

   197   ML_file "ProgLang/evaluate.sml"       (* requires setup from calculate.thy                    *)

   198   ML_file "ProgLang/listC.sml"

   199   ML_file "ProgLang/prog_expr.sml"

   200   ML_file "ProgLang/program.sml"

   201   ML_file "ProgLang/prog_tac.sml"

   202   ML_file "ProgLang/tactical.sml"

   203   ML_file "ProgLang/auto_prog.sml"

   204 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------

   205   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)

   207 subsection \<open>basic functionality on simple example first\<close>

   208   ML_file "Minisubpbl/000-comments.sml"

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

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

   211   ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"

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

   213   ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"

   214   ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"

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

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

   217   ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"

   218   ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"

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

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

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

   222   ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"

   223   ML_file "Minisubpbl/600-postcond.sml"

   224   ML_file "Minisubpbl/700-interSteps.sml"

   225   ML_file "Minisubpbl/710-interSteps-short.sml"

   226   ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"

   227   ML_file "Minisubpbl/790-complete.sml"

   228   ML_file "Minisubpbl/800-append-on-Frm.sml"

   230 subsection \<open>further functionality alongside batch build sequence\<close>

   231   ML_file "MathEngBasic/thmC.sml"

   232   ML_file "MathEngBasic/rewrite.sml"

   233   ML_file "MathEngBasic/tactic.sml"

   234 (*ML_file "MathEngBasic/ctree.sml"  TOODOO Isa hangs ?!?*)

   235   ML_file "MathEngBasic/calculation.sml"

   237   ML_file "Specify/formalise.sml"

   238   ML_file "Specify/o-model.sml"

   239   ML_file "Specify/i-model.sml"

   240   ML_file "Specify/pre-conditions.sml"

   241   ML_file "Specify/p-model.sml"

   242   ML_file "Specify/m-match.sml"

   243   ML_file "Specify/refine.sml"        (* requires setup from refine.thy *)

   244   ML_file "Specify/test-out.sml"

   245   ML_file "Specify/specify-step.sml"

   246   ML_file "Specify/specification.sml"

   247   ML_file "Specify/cas-command.sml"

   248   ML_file "Specify/p-spec.sml"

   249   ML_file "Specify/specify.sml"

   250   ML_file "Specify/step-specify.sml"

   252   ML_file "Interpret/istate.sml"

   253   ML_file "Interpret/sub-problem.sml"

   254   ML_file "Interpret/error-pattern.sml"

   255   ML_file "Interpret/li-tool.sml"

   256   ML_file "Interpret/lucas-interpreter.sml"

   257   ML_file "Interpret/step-solve.sml"

   259   ML_file "MathEngine/me-misc.sml"

   260   ML_file "MathEngine/fetch-tactics.sml"

   261   ML_file "MathEngine/solve.sml"

   262   ML_file "MathEngine/step.sml"

   263   ML_file "MathEngine/mathengine-stateless.sml"    (*!part. WN130804: +check Interpret/me.sml*)

   264   ML_file "MathEngine/messages.sml"

   265   ML_file "MathEngine/states.sml"

   267   ML_file "BridgeLibisabelle/thy-present.sml"

   268   ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)

   269   ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"

   270   ML_file "BridgeLibisabelle/thy-hierarchy.sml"

   271   ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)

   272 (** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free*)

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

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

   276   ML_file "BridgeJEdit/parseC.sml"

   277   ML_file "BridgeJEdit/preliminary.sml"

   279   ML_file "Knowledge/delete.sml"

   280   ML_file "Knowledge/descript.sml"

   281   ML_file "Knowledge/simplify.sml"

   282   ML_file "Knowledge/poly.sml"

   283 ML \<open>

   284 \<close> ML \<open>

   285 \<close> ML \<open>

   286 \<close> ML \<open>

   287 \<close> ML \<open>

   288 \<close> ML \<open>

   289 \<close> ML \<open>

   290 \<close> ML \<open>

   291 \<close> ML \<open>

   292 \<close> ML \<open>

   293 \<close> ML \<open>

   294 \<close>

   295   ML_file "Knowledge/gcd_poly_ml.sml"

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

   297   ML_file "Knowledge/rational.sml"                                            (*Test_Isac_Short*)

   298   ML_file "Knowledge/equation.sml"

   299   ML_file "Knowledge/root.sml"

   300   ML_file "Knowledge/lineq.sml"

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

   303 (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)

   304   ML_file "Knowledge/r/ootrat.sml"

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

   306 (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)

   307   ML_file "Knowledge/polyeq-1.sml"

   308 (*ML_file "Knowledge/polyeq-2.sml"                                              Test_Isac_Short*)

   309 (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)

   310   ML_file "Knowledge/calculus.sml"

   311   ML_file "Knowledge/trig.sml"

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

   313   ML_file "Knowledge/diff.sml"

   314   ML_file "Knowledge/integrate.sml"

   315   ML_file "Knowledge/eqsystem.sml"

   316   ML_file "Knowledge/test.sml"

   317   ML_file "Knowledge/polyminus.sml"

   318   ML_file "Knowledge/vect.sml"

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

   320   ML_file "Knowledge/biegelinie-1.sml"

   321 (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)

   322 (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)

   323   ML_file "Knowledge/biegelinie-4.sml"

   324   ML_file "Knowledge/algein.sml"

   325   ML_file "Knowledge/diophanteq.sml"

   326 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)

   327   ML_file "Knowledge/inssort.sml"

   328   ML_file "Knowledge/isac.sml"

   329   ML_file "Knowledge/build_thydata.sml"

   331   ML_file "Test_Code/test-code.sml"

   333 section \<open>further tests additional to src/.. files\<close>

   334   ML_file "BridgeLibisabelle/use-cases.sml"

   336   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>

   337   ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>

   338   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>

   339 ML \<open>

   340 \<close> ML \<open>

   341 \<close> ML \<open>

   342 \<close> ML \<open>

   343 \<close> ML \<open>

   344 \<close> ML \<open>

   345 \<close> ML \<open>

   346 \<close> ML \<open>

   347 \<close> ML \<open>

   348 \<close> ML \<open>

   349 \<close> ML \<open>

   350 \<close>

   352 section \<open>history of tests\<close>

   353 text \<open>

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

   355   Sanity of the regression tests suffers from updates following Isabelle development,

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

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

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

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

   362       with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   363 \<close>

   366 subsection \<open>isac on Isabelle2017\<close>

   367 subsubsection \<open>Summary of development\<close>

   368 text \<open>

   369   * Add further signatures, separate structures and cleanup respective files.

   370   * Show feasibility of moving Isac programs to partial_function, i.e. to the function package.

   371   * Clean theory dependencies.

   372   * Start preparing shift from isac-java to Isabelle/jEdit.

   373 \<close>

   374 subsubsection \<open>State of tests: unchanged\<close>

   375 subsubsection \<open>Changesets of begin and end\<close>

   376 text \<open>

   377   last changeset with Test_Isac 925fef0f4c81

   378   first changeset with Test_Isac bbb414976dfe

   379 \<close>

   381 subsection \<open>isac on Isabelle2015\<close>

   382 subsubsection \<open>Summary of development\<close>

   383 text \<open>

   384   * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).

   385     This complicates Test_Isac, see "Prepare running tests" above.

   386   * Remove TTY interface.

   387   * Re-activate insertion sort.

   388 \<close>

   389 subsubsection \<open>State of tests: unchanged\<close>

   390 subsubsection \<open>Changesets of begin and end\<close>

   391 text \<open>

   392   last changeset with Test_Isac 2f1b2854927a

   393   first changeset with Test_Isac ???

   394 \<close>

   396 subsection \<open>isac on Isabelle2014\<close>

   397 subsubsection \<open>Summary of development\<close>

   398 text \<open>

   399   migration from "isabelle tty" --> libisabelle

   400 \<close>

   402 subsection \<open>isac on Isabelle2013-2\<close>

   403 subsubsection \<open>Summary of development\<close>

   404 text \<open>

   405   reactivated context_thy

   406 \<close>

   407 subsubsection \<open>State of tests\<close>

   408 text \<open>

   409   TODO

   410 \<close>

   411 subsubsection \<open>Changesets of begin and end\<close>

   412 text \<open>

   413   TODO

   414   :

   415   : isac on Isablle2013-2

   416   :

   417   Changeset: 55318 (03826ceb24da) merged

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

   419   Date: 2013-12-12 14:27:37 +0100 (7 minutes)

   420 \<close>

   422 subsection \<open>isac on Isabelle2013-1\<close>

   423 subsubsection \<open>Summary of development\<close>

   424 text \<open>

   425   Isabelle2013-1 was replaced within a few weeks due to problems with the document model;

   426   no significant development steps for ISAC.

   427 \<close>

   428 subsubsection \<open>State of tests\<close>

   429 text \<open>

   430   See points in subsection "isac on Isabelle2011", "State of tests".

   431 \<close>

   432 subsubsection \<open>Changesets of begin and end\<close>

   433 text \<open>

   434   Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy

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

   436   Date: 2013-12-03 18:13:31 +0100 (8 days)

   437   :

   438   : isac on Isablle2013-1

   439   :

   440   Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect

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

   442   Date: 2013-11-21 18:12:17 +0100 (2 weeks)

   444 \<close>

   446 subsection \<open>isac on Isabelle2013\<close>

   447 subsubsection \<open>Summary of development\<close>

   448 text \<open>

   449   # Oct.13: replaced "axioms" by "axiomatization"

   450   # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref

   451   # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into

   452     simplification of multivariate rationals (without improving the rulesets involved).

   453 \<close>

   454 subsubsection \<open>Run tests\<close>

   455 text \<open>

   456   Is standard now; this subsection will be discontinued under Isabelle2013-1

   457 \<close>

   458 subsubsection \<open>State of tests\<close>

   459 text \<open>

   460   See points in subsection "isac on Isabelle2011", "State of tests".

   461   # re-activated listC.sml

   462 \<close>

   463 subsubsection \<open>Changesets of begin and end\<close>

   464 text \<open>

   465   changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"

   466   User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>

   467   Date: Tue Nov 19 22:23:30 2013 +0000

   468   :

   469   : isac on Isablle2013

   470   :

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

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

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

   474 \<close>

   476 subsection \<open>isac on Isabelle2012\<close>

   477 subsubsection \<open>Summary of development\<close>

   478 text \<open>

   479   isac on Isabelle2012 is considered just a transitional stage

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

   481   For considerations on the transition see

   482   $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".

   483 \<close>

   484 subsubsection \<open>Run tests\<close>

   485 text \<open>

   486 $ cd /usr/local/isabisac12/

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

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

   489 \<close>

   490 subsubsection \<open>State of tests\<close>

   491 text \<open>

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

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

   494   in parallel with evaluation.

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

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

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

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

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

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

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

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

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

   507 \<close>

   508 subsubsection \<open>Changesets of begin and end\<close>

   509 text \<open>

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

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

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

   513   :

   514   : isac on Isablle2012

   515   :

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

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

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

   519   ------------------------------------------------------------------------------

   520   Changeset: 48756 (7443906996a8) merged

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

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

   523 \<close>

   525 subsection \<open>isac on Isabelle2011\<close>

   526 subsubsection \<open>Summary of development\<close>

   527 text \<open>

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

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

   530   (2) Z_Transform was introduced by Jan Rocnik, which revealed

   531     further errors introduced by (1).

   532   (3) "error patterns" were introduced by Gabriella Daroczy

   533   Regressions tests have been added for all of these.

   534 \<close>

   535 subsubsection \<open>Run tests\<close>

   536 text \<open>

   537   $ cd /usr/local/isabisac11/

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

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

   540 \<close>

   541 subsubsection \<open>State of tests\<close>

   542 text \<open>

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

   544   and sometimes give reasons for failing tests.

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

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

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

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

   550   ------------------------------------------------------------------------------

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

   552   ------------------------------------------------------------------------------

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

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

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

   558   The list below records TODOs while producing an ISAC kernel for

   559   gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING

   560   (so to be resumed with Isabelle2013-1):

   561   ############## WNxxxxxx.TODO can be found in sources ##############

   562   --------------------------------------------------------------------------------

   563   WN111013.TODO: lots of cleanup/removal in test/../Test.thy

   564   --------------------------------------------------------------------------------

   565   WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with

   566   this special case (see) --- why not nxt = Model_Problem here ? ---

   567   --------------------------------------------------------------------------------

   568   WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/

   569   ... FIRST redesign

   570   # simplify_* , *_simp_*

   571   # norm_*

   572   # calc_* , calculate_*  ... require iteration over all rls ...

   573   ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !

   574   --------------------------------------------------------------------------------

   575   WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!

   576   --------------------------------------------------------------------------------

   577   WN120314 changeset a393bb9f5e9f drops root equations.

   578   see test/Tools/isac/Knowledge/rootrateq.sml

   579   --------------------------------------------------------------------------------

   580   WN120317.TODO changeset 977788dfed26 dropped rateq:

   581   # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002

   582   # test --- solve (1/x = 5, x) by me --- and --- x / (x  \<up>  2 - 6 * x + 9) - ...:

   583     investigation Check_elementwise stopped due to too much effort finding out,

   584     why Check_elementwise worked in 2002 in spite of the error.

   585   --------------------------------------------------------------------------------

   586   WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl

   587   --------------------------------------------------------------------------------

   588   WN120317.TODO found by test --- interSteps for Schalk 299a --- that

   589     NO test with 'interSteps' is checked properly (with exn on changed behaviour)

   590   --------------------------------------------------------------------------------

   591   WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has

   592     a newly outcommented test where rewrite_set_ make_polynomial --> NONE

   593   --------------------------------------------------------------------------------

   594   WN120320.TODO check-improve rlsthmsNOTisac:

   595   DONE make test --- old compute rlsthmsNOTisac by eq_thmI'

   596   DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy

   597   FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab

   598   # mark twice thms (in isac + (later) in Isabelle) in Isac.thy

   599   --------------------------------------------------------------------------------

   600   WN120320.TODO rlsthmsNOTisac: replace twice thms  \<up>

   601   --------------------------------------------------------------------------------

   602   WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test

   603   --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.

   604   --------------------------------------------------------------------------------

   605   WN120321.TODO rearrange theories:

   606     Knowledge

   607       :

   608       Prog_Expr.thy

   609       ///Input_Descript.thy --> ProgLang

   610       Delete.thy   <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)

   611     ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy

   612           Interpret.thy are generated (simplifies xml structure for theories)

   613       Program.thy

   614       Tools.thy

   615       ListC.thy    <--- first_Proglang_thy

   616   --------------------------------------------------------------------------------

   617   WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify

   618       EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"

   619   broken during work on thy-hierarchy

   620   --------------------------------------------------------------------------------

   621   WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see

   622   test --- the_hier (get_thes ()) (collect_thydata ())---

   623   --------------------------------------------------------------------------------

   624   WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_

   625   !!add mutual crossreferences to ?fun headline??? where the same has to be done:

   626   !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!

   627   --------------------------------------------------------------------------------

   628   WN120411 scanning html representation of newly generated knowledge:

   629   * thy:

   630   ** Theorems: only "Proof of the theorem" (correct!)

   631                and "(c) isac-team (math-autor)"

   632   ** Rulesets: only "Identifier:///"

   633                and "(c) isac-team (math-autor)"

   634   ** IsacKnowledge: link to dependency graph (which needs to be created first)

   635   ** IsacScripts --> ProgramLanguage

   636   *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen

   638   * pbl: OK !?!

   639   * met: OK !?!

   640   * exp:

   641   ** Z-Transform is missing !!!

   642   ** type-constraints !!!

   643   --------------------------------------------------------------------------------

   644   WN120417: merging xmldata revealed:

   645   ..............NEWLY generated:........................................

   646   <THEOREMDATA>

   647     <GUH> thy_isab_Fun-thm-o_apply </GUH>

   648     <STRINGLIST>

   649       <STRING> Isabelle </STRING>

   650       <STRING> Fun </STRING>

   651       <STRING> Theorems </STRING>

   652       <STRING> o_apply </STRING>

   653     </STRINGLIST>

   654       <MATHML>

   655         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>

   656       </MATHML>  <PROOF>

   657       <EXTREF>

   658         <TEXT> Proof of the theorem </TEXT>

   659         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>

   660       </EXTREF>

   661     </PROOF>

   662     <EXPLANATIONS> </EXPLANATIONS>

   663     <MATHAUTHORS>

   664       <STRING> Isabelle team, TU Munich </STRING>

   665     </MATHAUTHORS>

   666     <COURSEDESIGNS>

   667     </COURSEDESIGNS>

   668   </THEOREMDATA>

   669   ..............OLD FORMAT:.............................................

   670   <THEOREMDATA>

   671     <GUH> thy_isab_Fun-thm-o_apply </GUH>

   672     <STRINGLIST>

   673       <STRING> Isabelle </STRING>

   674       <STRING> Fun </STRING>

   675       <STRING> Theorems </STRING>

   676       <STRING> o_apply </STRING>

   677     </STRINGLIST>

   678     <THEOREM>

   679       <ID> o_apply </ID>

   680       <MATHML>

   681         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>

   682       </MATHML>

   683     </THEOREM>

   684     <PROOF>

   685       <EXTREF>

   686         <TEXT> Proof of the theorem </TEXT>

   687         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>

   688       </EXTREF>

   689     </PROOF>

   690     <EXPLANATIONS> </EXPLANATIONS>

   691     <MATHAUTHORS>

   692       <STRING> Isabelle team, TU Munich </STRING>

   693     </MATHAUTHORS>

   694     <COURSEDESIGNS>

   695     </COURSEDESIGNS>

   696   </THEOREMDATA>

   697   --------------------------------------------------------------------------------

   698 \<close>

   699 subsubsection \<open>Changesets of begin and end\<close>

   700 text \<open>

   701   isac development was done between these changesets:

   702   ------------------------------------------------------------------------------

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

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

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

   706   :

   707   : isac on Isablle2011

   708   :

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

   710   Branch: decompose-isar

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

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

   713   ------------------------------------------------------------------------------

   714 \<close>

   716 subsection \<open>isac on Isabelle2009-2\<close>

   717 subsubsection \<open>Summary of development\<close>

   718 text \<open>

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

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

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

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

   723 \<close>

   724 subsubsection \<open>Run tests\<close>

   725 text \<open>

   726   WN131021 this is broken by installation of Isabelle2011/12/13,

   727   because all these write their binaries to ~/.isabelle/heaps/..

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

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

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

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

   733 \<close>

   734 subsubsection \<open>State of tests\<close>

   735 text \<open>

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

   737 \<close>

   738 subsubsection \<open>Changesets of begin and end\<close>

   739 text \<open>

   740   isac development was done between these changesets:

   741   ------------------------------------------------------------------------------

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

   743   Branch: decompose-isar

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

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

   746   :

   747   : isac on Isablle2009-2

   748   :

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

   750   Branch: isac-from-Isabelle2009-2

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

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

   753   ------------------------------------------------------------------------------

   754 \<close>

   756 subsection \<open>isac on Isabelle2002\<close>

   757 subsubsection \<open>Summary of development\<close>

   758 text \<open>

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

   760   of isac's mathematics engine has been implemented.

   761 \<close>

   762 subsubsection \<open>Run tests\<close>

   763 subsubsection \<open>State of tests\<close>

   764 text \<open>

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

   766   recent Linux versions)

   767 \<close>

   768 subsubsection \<open>Changesets of begin and end\<close>

   769 text \<open>

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

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

   772 \<close>

   774 end

   775 (*========== inhibit exn 130719 Isabelle2013 ===================================

   776 ============ inhibit exn 130719 Isabelle2013 =================================*)

   778 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   779   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

author	wneuper <walther.neuper@jku.at>
	Thu, 15 Jul 2021 20:09:44 +0200
changeset 60326	33e04eb1a2f0
parent 60325	a7c0e6ab4883
child 60329	0c10aeff57d7
permissions	-rw-r--r--