neuper@52065: (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) neuper@41943: Author: Walther Neuper 101001 wneuper@59258: (c) copyright due to license 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 wneuper@59323: ------------------------------------------------------------------------------- neuper@52065: wneuper@59323: Prepare running tests: see below wneuper@59323: Run tests: neuper@52065: $ cd /usr/local/isabisac/ wneuper@59323: $ export ISABELLE_VERSION=2015 # for libisabelle neuper@52065: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & neuper@41943: *) neuper@41943: wneuper@59258: section \Prepare running tests\ wneuper@59258: text \ wneuper@59323: Isac encapsulates code as much as possible in structures without open. TODO ProgLang. wneuper@59258: This policy conflicts with those tests, which go into functions to details wneuper@59258: not declared in the signatures. wneuper@59258: wneuper@59258: In order to maintain these tests without changes, this has to be done before running tests: wneuper@59323: (1) Extend signatures for tests by wneuper@59323: ~~$ ./xcoding-to-test.sh wneuper@59323: ~~$ ./zcoding-to-test.sh # -"- + go back to Test_Isac.thy wneuper@59323: Running Test_Isac.thy opens all structures, see code after "begin" below. wneuper@59323: (2) Clean signatures for coding wneuper@59323: ~~$ ./xtest-to-coding.sh wneuper@59323: ~~$ ./xtest-to-coding.sh # -"- + go back to coding (!update thy!) wneuper@59323: wneuper@59323: ********************* don't forget (2) BEFORE pushing to repository ********************* wneuper@59323: wneuper@59323: The above bash files accomplish query replace in src/Tools/isac: wneuper@59261: \--- ! aktivate for Test_Isac BEGIN ---\* )\ \ \--- ! aktivate for Test_Isac BEGIN ---\*)\ wneuper@59261: \( *\--- ! aktivate for Test_Isac END ---\ \ \(*\--- ! aktivate for Test_Isac END ---\ wneuper@59261: ^^^ in signature outcommented, ^^^ NOT outcommented, wneuper@59261: this is status for coding this is status for tests wneuper@59258: \ wneuper@59258: wneuper@59366: section \code for copy & paste\ wneuper@59366: text \ wneuper@59366: "~~~~~ fun , args:"; val () = (); wneuper@59366: "~~~~~ and , args:"; val () = (); wneuper@59366: wneuper@59366: "~~~~~ to return val:"; val () = (); wneuper@59366: wneuper@59366: \ wneuper@59258: section \Run the tests\ wneuper@59258: text \ wneuper@59258: * say "OK" to the popup asking for theories to be loaded wneuper@59258: * watch the window for errors in the "imports" below wneuper@59258: \ neuper@52073: wneuper@59410: theory Test_Isac imports Build_Thydata (* note that imports are WITHOUT open struct ..*) wneuper@59364: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) neuper@52116: "ADDTESTS/accumulate-val/Thy_All" neuper@41980: "ADDTESTS/Ctxt" neuper@42048: "ADDTESTS/test-depend/Build_Test" neuper@42023: "ADDTESTS/All_Ctxt" wneuper@59202: "ADDTESTS/Test_Units" 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" wneuper@59144: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" wneuper@59144: ADDTESTS/------------------------------------------- see end of tests *) wneuper@59194: (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *) neuper@52089: (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*) neuper@52073: "~~/test/Pure/Isar/Test_Parse_Term" wneuper@59364: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) neuper@55364: "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *) neuper@55366: "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*) wneuper@59388: wneuper@59388: wneuper@59388: wneuper@59362: "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *) s1210629013@55377: "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) wneuper@59364: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) 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*) wneuper@59364: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) neuper@52168: neuper@41943: begin s1210629013@55442: s1210629013@55446: ML {* wneuper@59258: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*) wneuper@59318: (* these vvv test, if funs are intermediately opened in structure wneuper@59318: in case of errors here consider ~~/./xtest-to-coding.sh *) wneuper@59261: open Kernel; wneuper@59262: open Math_Engine; CalcTreeTEST; wneuper@59262: open Lucin; appy; wneuper@59262: open Inform; cas_input; wneuper@59263: open Rtools; trtas2str; wneuper@59265: open Chead; pt_extract; wneuper@59316: open Generate; (* NONE *) wneuper@59276: open Ctree; append_problem; wneuper@59269: open Specify; show_ptyps; wneuper@59316: open Applicable; mk_set; wneuper@59316: open Solve; (* NONE *) wneuper@59299: open Selem; e_fmz; wneuper@59308: open Stool; transfer_asms_from_to; wneuper@59316: open Tac; (* NONE *) wneuper@59316: open Model; (* NONE *) wneuper@59384: open LTool; rule2stac; wneuper@59384: open Rewrite; mk_thm; wneuper@59388: open Calc; get_pair; wneuper@59410: open TermC; atomt; wneuper@59417: open Celem; e_pbt; wneuper@59417: open Rule; string_of_thm; wneuper@59258: (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59258: *} wneuper@59366: wneuper@59258: ML {* wneuper@59366: "~~~~~ fun xxx, args:"; val () = (); wneuper@59356: *} ML {* wneuper@59356: *} ML {* wneuper@59356: *} wneuper@59356: wneuper@59356: ML {* s1210629013@55446: KEStore_Elems.set_ref_thy @{theory}; wneuper@59248: (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); s1210629013@55446: *} s1210629013@55442: wneuper@59372: (*---------------------- check test file by testfile ------------------------------------------- wneuper@59372: ---------------------- check test file by testfile -------------------------------------------*) 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" wneuper@59115: ML_file "~~/test/Pure/PIDE/xml.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" wneuper@59356: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59388: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) wneuper@59356: ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) wneuper@59357: ML_file "ProgLang/termC.sml" wneuper@59359: ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) wneuper@59358: 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" wneuper@59362: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59366: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) 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" wneuper@59411: ML_file "Minisubpbl/250-Rewrite_Set-from-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 %%%%%%%%%%%%%%%%%%%%%%%";*} wneuper@59364: ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} neuper@52065: ML_file "Interpret/mstools.sml" neuper@52065: ML_file "Interpret/ctree.sml" (*!...!see(25)*) neuper@55364: ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *) neuper@48891: ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *} neuper@52065: ML_file "Interpret/generate.sml" neuper@52065: ML_file "Interpret/calchead.sml" wneuper@59252: ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *) wneuper@55498: ML_file "Interpret/rewtools.sml" neuper@52065: ML_file "Interpret/script.sml" neuper@52065: ML_file "Interpret/solve.sml" neuper@52065: ML_file "Interpret/inform.sml" 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@55408: ML_file "xmlsrc/thy-hierarchy.sml" wneuper@59429: 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" wneuper@59370: ML_file "Knowledge/gcd_poly_ml.sml" wneuper@59370: ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) wneuper@59370: ML_file "Knowledge/rational.sml" wneuper@59370: ML_file "Knowledge/equation.sml" wneuper@59370: ML_file "Knowledge/root.sml" wneuper@59370: ML_file "Knowledge/lineq.sml" wneuper@59370: (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) wneuper@59370: ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) wneuper@59370: ML_file "Knowledge/rootrat.sml" wneuper@59370: 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. *) wneuper@59372: ML_file "Knowledge/biegelinie-1.sml" wneuper@59412: (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *) 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" wneuper@59232: ML_file "Knowledge/inssort.sml" neuper@52065: ML_file "Knowledge/isac.sml" neuper@52065: ML_file "Knowledge/build_thydata.sml" neuper@48895: ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*} wneuper@59144: ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*} wneuper@59144: ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" wneuper@59175: ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" wneuper@59144: ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*} wneuper@59144: wneuper@59144: ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} wneuper@59144: ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*} 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: wneuper@59323: wneuper@59323: subsection {* isac on Isabelle2015 *} wneuper@59323: subsubsection {* Summary of development *} wneuper@59323: text {* wneuper@59373: * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang). wneuper@59323: This complicates Test_Isac, see "Prepare running tests" above. wneuper@59323: * Remove TTY interface. wneuper@59323: * Re-activate insertion sort. wneuper@59323: *} wneuper@59323: subsubsection {* State of tests: unchanged *} wneuper@59323: subsubsection {* Changesets of begin and end *} wneuper@59323: text {* wneuper@59323: last changeset with Test_Isac 2f1b2854927a wneuper@59323: first changeset with Test_Isac ??? wneuper@59323: *} wneuper@59323: wneuper@59120: subsection {* isac on Isabelle2014 *} wneuper@59120: subsubsection {* Summary of development *} wneuper@59120: text {* wneuper@59120: migration from "isabelle tty" --> libisabelle wneuper@59120: *} wneuper@59120: neuper@55319: subsection {* isac on Isabelle2013-2 *} neuper@55319: subsubsection {* Summary of development *} neuper@55319: text {* wneuper@55500: reactivated context_thy 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@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@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@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 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@52079: Date: 2013-07-15 08:28:50 +0200 (4 weeks) neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2012 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: isac on Isabelle2012 is considered just a transitional stage neuper@48895: within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; neuper@48895: For considerations on the transition see neuper@48895: ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..". neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@48895: $ cd /usr/local/isabisac12/ neuper@48895: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy neuper@48895: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy neuper@48895: *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: At least the tests from isac on Isabelle2011 run again. neuper@48895: However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling neuper@48895: in parallel with evaluation. neuper@48895: neuper@48895: Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant) neuper@48895: yields 69 hits, some of which were already present before Isabelle2002-->2009-2 neuper@48895: (i.e. on the old notebook from 2002). neuper@48895: neuper@48895: Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin: neuper@48895: # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy neuper@48895: # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002 neuper@48895: # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002 neuper@48895: Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml. neuper@48895: neuper@48895: Some tests have been re-activated (e.g. error patterns, fill patterns). neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@52079: text {* neuper@52079: Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012 neuper@52079: User: Walther Neuper neuper@52079: Date: 2013-07-11 16:58:31 +0200 (4 weeks) neuper@48895: : neuper@48895: : isac on Isablle2012 neuper@48895: : neuper@48895: Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012 neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-09-24 18:35:13 +0200 (8 months) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: Changeset: 48756 (7443906996a8) merged neuper@48895: User: Walther Neuper neuper@48895: Date: 2012-09-24 18:15:49 +0200 (8 months) neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2011 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: isac's mathematics engine has been extended by two developments: neuper@48895: (1) Isabelle's contexts were introduced by Mathias Lehnfeld neuper@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@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@55421: test --- the_hier (get_thes ()) (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: neuper@52150: thy_isab_Fun-thm-o_apply neuper@52150: neuper@52150: Isabelle neuper@52150: Fun neuper@52150: Theorems neuper@52150: o_apply neuper@52150: neuper@52150: neuper@52150: (?f o ?g) ?x = ?f (?g ?x) neuper@52150: neuper@52150: neuper@52150: Proof of the theorem neuper@52150: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html neuper@52150: neuper@52150: neuper@52150: neuper@52150: neuper@52150: Isabelle team, TU Munich neuper@52150: neuper@52150: neuper@52150: neuper@52150: neuper@52150: ..............OLD FORMAT:............................................. neuper@52150: neuper@52150: thy_isab_Fun-thm-o_apply neuper@52150: neuper@52150: Isabelle neuper@52150: Fun neuper@52150: Theorems neuper@52150: o_apply neuper@52150: neuper@52150: neuper@52150: o_apply neuper@52150: neuper@52150: (?f o ?g) ?x = ?f (?g ?x) neuper@52150: neuper@52150: neuper@52150: neuper@52150: neuper@52150: Proof of the theorem neuper@52150: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html neuper@52150: neuper@52150: neuper@52150: neuper@52150: neuper@52150: Isabelle team, TU Munich neuper@52150: neuper@52150: neuper@52150: neuper@52150: 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@48895: Date: 2012-09-24 16:39:30 +0200 (8 months) neuper@48895: : neuper@48895: : isac on Isablle2011 neuper@48895: : neuper@48895: Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011 neuper@48895: Branch: decompose-isar neuper@48895: User: Walther Neuper neuper@48895: Date: 2011-02-25 13:04:56 +0100 (2011-02-25) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2009-2 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg. neuper@48895: The update was painful (bridging 7 years of Isabelle development) and cut short neuper@48895: due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and neuper@48895: going on to Isabelle2011 although most of the tests did not run. neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: text {* neuper@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 neuper@48895: Date: 2011-02-06 18:30:28 +0100 (2011-02-06) neuper@48895: : neuper@48895: : isac on Isablle2009-2 neuper@48895: : neuper@48895: Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 neuper@48895: Branch: isac-from-Isabelle2009-2 neuper@48895: User: Walther Neuper neuper@48895: Date: 2010-07-21 09:59:35 +0200 (2010-07-21) neuper@48895: ------------------------------------------------------------------------------ neuper@48895: *} neuper@48895: neuper@48895: subsection {* isac on Isabelle2002 *} neuper@48895: subsubsection {* Summary of development *} neuper@48895: text {* neuper@48895: From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern") neuper@48895: of isac's mathematics engine has been implemented. neuper@48895: *} neuper@48895: subsubsection {* Run tests *} neuper@48895: subsubsection {* State of tests *} neuper@48895: text {* neuper@48895: All tests work on an old notebook (the right PolyML coudn't be upgraded to more neuper@48895: recent Linux versions) neuper@48895: *} neuper@48895: subsubsection {* Changesets of begin and end *} neuper@48895: text {* neuper@48895: Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS; neuper@48895: see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial. neuper@48895: *} neuper@48895: neuper@41943: end neuper@52065: (*========== inhibit exn 130719 Isabelle2013 =================================== neuper@52065: ============ inhibit exn 130719 Isabelle2013 =================================*) neuper@41943: neuper@41943: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@48895: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@41975: