
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@52101:    Isac's tests are organised parallel to sources: 
neuper@52101:      "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
neuper@52101:    plus
neuper@52065:      ~~/test/Tools/isac/ADDTESTS
neuper@52101:      ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
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@52105: (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
neuper@52139: (* !!!!! say "OK" to the popup asking for theories to be loaded and !!!!!!!!!!!!! *)
neuper@52139: (* !!!!! watch the <Theories> window for errors in the "imports" below !!!!!!!!!! *)
neuper@52105: (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
neuper@52073: 
neuper@52067: theory Test_Isac imports Isac
neuper@52116:   "ADDTESTS/accumulate-val/Thy_All"
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@52102:   "ADDTESTS/session-get_theory/Foo"
neuper@52101: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*)
neuper@52073:   "~~/test/Pure/Isar/Test_Parsers"
neuper@52089: (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
neuper@52073:   "~~/test/Pure/Isar/Test_Parse_Term"
neuper@52073:   "~~/test/HOL/Library/Test_Polynomial"
neuper@52073: 
neuper@52168:   "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
neuper@52168:   "~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)
neuper@52168: 
neuper@41943: begin
neuper@52119: section {* trials with Isabelle's functions *}
neuper@52119:   ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@52119:   ML_file "~~/test/Pure/General/alist.ML"
neuper@52119:   ML_file "~~/test/Pure/General/basics.ML"
neuper@52119:   ML_file "~~/test/Pure/General/scan.ML"
neuper@52119:   ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@52119: 
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@52126:   ML_file          "kestore.sml"
neuper@52065:   ML_file "ProgLang/termC.sml"
neuper@52065:   ML_file "ProgLang/calculate.sml"
neuper@52065:   ML_file "ProgLang/rewrite.sml"
neuper@52148:   ML_file "ProgLang/listC.sml"
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@52105:   ML_file "Interpret/mathengine.sml"    (*!part. WN130804: +check Interpret/me.sml*)
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@52112:   ML_file "Frontend/use-cases.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@52088:   ML_file "Knowledge/gcd_poly_ml.sml"
neuper@52088:   ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
neuper@52088:   ML_file "Knowledge/rational.sml"
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@52105:   ML_file "Knowledge/polyeq.sml"
neuper@52105: (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
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@52065:   ML_file "Knowledge/isac.sml"
neuper@52065:   ML_file "Knowledge/build_thydata.sml"
neuper@48895:   ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
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@52139:   Sanity of the regression tests suffers 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@55319: subsection {* isac on Isabelle2013-2 *}
neuper@55319: subsubsection {* Summary of development *}
neuper@55319: text {*
neuper@55319:   TODO
neuper@55319: *}
neuper@55319: subsubsection {* State of tests *}
neuper@55319: text {*
neuper@55319:   TODO
neuper@55319: *}
neuper@55319: subsubsection {* Changesets of begin and end *}
neuper@55319: text {*
neuper@55319:   TODO
neuper@55319:   :
neuper@55319:   : isac on Isablle2013-2
neuper@55319:   :
neuper@55319:   Changeset: 55318 (03826ceb24da) merged
neuper@55319:   User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55319:   Date: 2013-12-12 14:27:37 +0100 (7 minutes)
neuper@55319: *}
neuper@55319: 
neuper@55284: subsection {* isac on Isabelle2013-1 *}
neuper@55284: subsubsection {* Summary of development *}
neuper@55284: text {*
neuper@55284:   Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
neuper@55284:   no significant development steps for ISAC.
neuper@55284: *}
neuper@55284: subsubsection {* State of tests *}
neuper@55284: text {*
neuper@55284:   See points in subsection "isac on Isabelle2011", "State of tests".
neuper@55284: *}
neuper@55284: subsubsection {* Changesets of begin and end *}
neuper@55284: text {*
neuper@55284:   Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
neuper@55284:   User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55284:   Date: 2013-12-03 18:13:31 +0100 (8 days)
neuper@55284:   :
neuper@55284:   : isac on Isablle2013-1
neuper@55284:   :
neuper@55284:   Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
neuper@55284:   User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55284:   Date: 2013-11-21 18:12:17 +0100 (2 weeks)
neuper@55284: 
neuper@55284: *}
neuper@55284: 
neuper@48895: subsection {* isac on Isabelle2013 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
neuper@52150:   # Oct.13: replaced "axioms" by "axiomatization"
neuper@52150:   # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
neuper@52106:   # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
neuper@52106:     simplification of multivariate rationals (without improving the rulesets involved).
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: text {*
neuper@52150:   Is standard now; this subsection will be discontinued under Isabelle2013-1
neuper@48895: *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {*
neuper@52150:   See points in subsection "isac on Isabelle2011", "State of tests".
neuper@52150:   # re-activated listC.sml
neuper@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
neuper@52175:   changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
neuper@52175:   User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
neuper@52175:   Date: Tue Nov 19 22:23:30 2013 +0000
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@ist.tugraz.at>
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@ist.tugraz.at>
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@ist.tugraz.at>
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@ist.tugraz.at>
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@52150:   (2) Z_Transform was introduced by Jan Rocnik, which revealed
neuper@52150:     further errors introduced by (1).
neuper@52150:   (3) "error patterns" were introduced by Gabriella Daroczy
neuper@52150:   Regressions tests have been added for all of these.
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:   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@ist.tugraz.at>
neuper@48895:   Date: 2012-08-06 10:38:11 +0200 (11 months)
neuper@52150: 
neuper@52150: 
neuper@52150:   The list below records TODOs while producing an ISAC kernel for 
neuper@52150:   gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
neuper@52150:   (so to be resumed with Isabelle2013-1):
neuper@52150:   ############## WNxxxxxx.TODO can be found in sources ##############
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN111013.TODO: lots of cleanup/removal in test/../Test.thy
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN111013.TODO: remove concept around "fun init_form", lots of troubles with 
neuper@52150:   this special case (see) --- why not nxt = Model_Problem here ? ---
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
neuper@52150:   ... FIRST redesign 
neuper@52150:   # simplify_* , *_simp_* 
neuper@52150:   # norm_* 
neuper@52150:   # calc_* , calculate_*  ... require iteration over all rls ...
neuper@52150:   ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120314 changeset a393bb9f5e9f drops root equations.
neuper@52150:   see test/Tools/isac/Knowledge/rootrateq.sml 
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120317.TODO changeset 977788dfed26 dropped rateq:
neuper@52150:   # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
neuper@52150:   # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:    
neuper@52150:     investigation Check_elementwise stopped due to too much effort finding out,
neuper@52150:     why Check_elementwise worked in 2002 in spite of the error.
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl 
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120317.TODO found by test --- interSteps for Schalk 299a --- that 
neuper@52150:     NO test with 'interSteps' is checked properly (with exn on changed behaviour)
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
neuper@52150:     a newly outcommented test where rewrite_set_ make_polynomial --> NONE
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120320.TODO check-improve rlsthmsNOTisac:
neuper@52150:   DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
neuper@52150:   DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy 
neuper@52150:   FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
neuper@52150:   # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120320.TODO rlsthmsNOTisac: replace twice thms ^
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
neuper@52150:   --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120321.TODO rearrange theories:
neuper@52150:     Knowledge
neuper@52150:       :
neuper@52150:       Atools.thy
neuper@52150:       ///Descript.thy --> ProgLang
neuper@52150:       Delete.thy   <--- first_Knowledge_thy (*mv to Atools.thy*)
neuper@52150:     ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
neuper@52150:           Interpret.thy are generated (simplifies xml structure for theories)
neuper@52150:       Script.thy
neuper@52150:       Tools.thy
neuper@52150:       ListC.thy    <--- first_Proglang_thy
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
neuper@52150:       EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
neuper@52150:   broken during work on thy-hierarchy
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
neuper@52150:   test --- the_hier (! thehier) (collect_thydata ())---
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
neuper@52150:   !!add mutual crossreferences to ?fun headline??? where the same has to be done:
neuper@52150:   !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120409.TODO replace "op mem" (2002) with member (2011) ... 
neuper@52150:   ... an exercise interesting for beginners !
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120411 scanning html representation of newly generated knowledge:
neuper@52150:   * thy:
neuper@52150:   ** Theorems: only "Proof of the theorem" (correct!)
neuper@52150:                and "(c) isac-team (math-autor)"
neuper@52150:   ** Rulesets: only "Identifier:///"
neuper@52150:                and "(c) isac-team (math-autor)"
neuper@52150:   ** IsacKnowledge: link to dependency graph (which needs to be created first)
neuper@52150:   ** IsacScripts --> ProgramLanguage
neuper@52150:   *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
neuper@52150:   
neuper@52150:   * pbl: OK !?!
neuper@52150:   * met: OK !?!
neuper@52150:   * exp: 
neuper@52150:   ** Z-Transform is missing !!!
neuper@52150:   ** type-constraints !!!
neuper@52150:   --------------------------------------------------------------------------------
neuper@52150:   WN120417: merging xmldata revealed:
neuper@52150:   ..............NEWLY generated:........................................
neuper@52150:   <THEOREMDATA>
neuper@52150:     <GUH> thy_isab_Fun-thm-o_apply </GUH>
neuper@52150:     <STRINGLIST>
neuper@52150:       <STRING> Isabelle </STRING>
neuper@52150:       <STRING> Fun </STRING>
neuper@52150:       <STRING> Theorems </STRING>
neuper@52150:       <STRING> o_apply </STRING>
neuper@52150:     </STRINGLIST>
neuper@52150:       <MATHML>
neuper@52150:         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
neuper@52150:       </MATHML>  <PROOF>
neuper@52150:       <EXTREF>
neuper@52150:         <TEXT> Proof of the theorem </TEXT>
neuper@52150:         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
neuper@52150:       </EXTREF>
neuper@52150:     </PROOF>
neuper@52150:     <EXPLANATIONS> </EXPLANATIONS>
neuper@52150:     <MATHAUTHORS>
neuper@52150:       <STRING> Isabelle team, TU Munich </STRING>
neuper@52150:     </MATHAUTHORS>
neuper@52150:     <COURSEDESIGNS>
neuper@52150:     </COURSEDESIGNS>
neuper@52150:   </THEOREMDATA>
neuper@52150:   ..............OLD FORMAT:.............................................
neuper@52150:   <THEOREMDATA>
neuper@52150:     <GUH> thy_isab_Fun-thm-o_apply </GUH>
neuper@52150:     <STRINGLIST>
neuper@52150:       <STRING> Isabelle </STRING>
neuper@52150:       <STRING> Fun </STRING>
neuper@52150:       <STRING> Theorems </STRING>
neuper@52150:       <STRING> o_apply </STRING>
neuper@52150:     </STRINGLIST>
neuper@52150:     <THEOREM>
neuper@52150:       <ID> o_apply </ID>
neuper@52150:       <MATHML>
neuper@52150:         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
neuper@52150:       </MATHML>
neuper@52150:     </THEOREM>
neuper@52150:     <PROOF>
neuper@52150:       <EXTREF>
neuper@52150:         <TEXT> Proof of the theorem </TEXT>
neuper@52150:         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
neuper@52150:       </EXTREF>
neuper@52150:     </PROOF>
neuper@52150:     <EXPLANATIONS> </EXPLANATIONS>
neuper@52150:     <MATHAUTHORS>
neuper@52150:       <STRING> Isabelle team, TU Munich </STRING>
neuper@52150:     </MATHAUTHORS>
neuper@52150:     <COURSEDESIGNS>
neuper@52150:     </COURSEDESIGNS>
neuper@52150:   </THEOREMDATA>
neuper@52150:   --------------------------------------------------------------------------------
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@ist.tugraz.at>
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@ist.tugraz.at>
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@52150:   WN131021 this is broken by installation of Isabelle2011/12/13,
neuper@52150:   because all these write their binaries to ~/.isabelle/heaps/..
neuper@52150: 
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: *}
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 <m.steger@student.tugraz.at>
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@ist.tugraz.at>
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: 




