wneuper@59553: (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) wneuper@59553: Author: Walther Neuper 101001 wneuper@59553: (c) copyright due to license terms. wneuper@59553: wneuper@59553: Isac's tests are organised parallel to sources: wneuper@59553: "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" wneuper@59553: plus wneuper@59553: ~~/test/Tools/isac/ADDTESTS wneuper@59553: ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality wneuper@59553: *) wneuper@59553: walther@59623: section \Notes on running tests\ walther@59623: subsection \Switch between running tests and updating code\ wneuper@59553: text \ walther@59623: Isac encapsulates code as much as possible in structures without open. walther@59623: This policy conflicts with those tests, which go into functions to details walther@59623: not declared in the signatures. walther@59623: walther@59623: In order to maintain these tests without changes, this has to be done before running tests: walther@59623: (1) Extend signatures for tests by walther@59623: ~~$ ./xcoding-to-test.sh walther@59623: ~~$ ./zcoding-to-test.sh # --"-- + go back to Test_Isac.thy walther@59623: Running Test_Isac.thy opens all structures, see code after "begin" below. walther@59623: (2) Clean signatures for coding walther@59623: ~~$ ./xtest-to-coding.sh walther@59623: ~~$ ./ztest-to-coding.sh # --"-- + go back to coding (!update thy!) wneuper@59553: walther@59623: ********************* don't forget (2) BEFORE pushing to repository **************************** walther@59623: \ walther@59623: subsection \Decide between running Test_Isac_Short.thy and Test_Isac.thy\ walther@59623: text \ walther@59623: Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml") walther@59623: if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default). walther@59626: This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences. walther@59626: A model is in the repository at ~~/etc/preferences. walther@59623: These preferences have drawbacks, however: walther@59623: * they claim more memory such that Isabelle instances canNOT run in parallel. walther@59623: * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there. wneuper@59553: walther@59623: So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode. walther@59623: From time to time full testing in Test_Isac.thy is recommended. For that purpose walther@59626: * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences. wneuper@59553: walther@59623: ********************* don't forget to re-set defaults BEFORE updating code ********************* walther@59623: walther@59626: Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use walther@59626: ***************** $ gedit ~/.isabelle/isabisac/etc/preferences & wneuper@59553: \ wneuper@59553: wneuper@59553: section \Run the tests\ wneuper@59553: text \ wneuper@59553: * say "OK" to the popup asking for theories to be loaded wneuper@59553: * watch the window for errors in the "imports" below wneuper@59553: \ wneuper@59553: walther@59623: theory Test_Isac_Short walther@59603: imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) wneuper@59553: "ADDTESTS/accumulate-val/Thy_All" wneuper@59553: "ADDTESTS/Ctxt" wneuper@59553: "ADDTESTS/test-depend/Build_Test" wneuper@59553: "ADDTESTS/All_Ctxt" wneuper@59553: "ADDTESTS/Test_Units" wneuper@59553: "ADDTESTS/course/phst11/T1_Basics" wneuper@59553: "ADDTESTS/course/phst11/T2_Rewriting" wneuper@59553: "ADDTESTS/course/phst11/T3_MathEngine" wneuper@59553: "ADDTESTS/file-depend/BuildC_Test" wneuper@59553: "ADDTESTS/session-get_theory/Foo" wneuper@59553: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" wneuper@59553: ADDTESTS/------------------------------------------- see end of tests *) wneuper@59553: (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *) wneuper@59553: (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*) wneuper@59553: "~~/test/Pure/Isar/Test_Parse_Term" wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) wneuper@59553: "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *) wneuper@59553: "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*) wneuper@59553: "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) wneuper@59553: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) wneuper@59556: (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*) wneuper@59556: (*"~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*) wneuper@59556: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) wneuper@59553: wneuper@59553: begin wneuper@59553: walther@59628: ML \open ML_System\ wneuper@59553: ML \ wneuper@59553: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*) wneuper@59553: (* these vvv test, if funs are intermediately opened in structure walther@59628: in case of errors here consider ~~/xtest-to-coding.sh *) wneuper@59553: open Kernel; wneuper@59553: open Math_Engine; CalcTreeTEST; wneuper@59556: open Lucin; itms2args; walther@59659: open Env; walther@59691: open LucinNEW; scan_dn2; walther@59617: open Istate; wneuper@59553: open Inform; cas_input; wneuper@59553: open Rtools; trtas2str; wneuper@59553: open Chead; pt_extract; wneuper@59553: open Generate; (* NONE *) wneuper@59553: open Ctree; append_problem; walther@59696: open Pos; walther@59618: open Program; wneuper@59601: open Prog_Tac; walther@59603: open Tactical; walther@59603: open Prog_Expr; walther@59618: open Auto_Prog; rule2stac; wneuper@59600: open Input_Descript; wneuper@59553: open Specify; show_ptyps; walther@59763: open SpecifyNEW; wneuper@59553: open Applicable; mk_set; walther@59763: open Step_Specify; walther@59749: open Step_Solve; walther@59763: open Step; wneuper@59553: open Solve; (* NONE *) wneuper@59553: open Selem; e_fmz; wneuper@59577: open Stool; (* NONE *) wneuper@59577: open ContextC; transfer_asms_from_to; walther@59728: open Tactic; insert_assumptions; wneuper@59553: open Model; (* NONE *) wneuper@59553: open Rewrite; mk_thm; wneuper@59553: open Calc; get_pair; wneuper@59553: open TermC; atomt; wneuper@59553: open Celem; e_pbt; wneuper@59553: open Rule; string_of_thm; wneuper@59553: (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59553: \ wneuper@59553: wneuper@59553: ML \ walther@59659: "~~~~~ fun xxx , args:"; val () = (); walther@59659: "~~~~~ and xxx , args:"; val () = (); walther@59723: "~~~~~ from fun xxx\fun yyy\fun zzz, return val:"; val () = (); walther@59659: (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); walther@59659: "xx" walther@59723: ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) walther@59723: \ ML \ walther@59723: \ walther@59723: ML \ walther@59723: \ ML \ wneuper@59553: \ ML \ wneuper@59553: \ wneuper@59553: wneuper@59553: ML \ wneuper@59553: KEStore_Elems.set_ref_thy @{theory}; wneuper@59553: (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); wneuper@59553: \ wneuper@59553: wneuper@59553: (*---------------------- check test file by testfile ------------------------------------------- wneuper@59553: ---------------------- check test file by testfile -------------------------------------------*) wneuper@59553: section \trials with Isabelle's functions\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML_file "~~/test/Pure/General/alist.ML" wneuper@59553: ML_file "~~/test/Pure/General/basics.ML" wneuper@59553: ML_file "~~/test/Pure/General/scan.ML" wneuper@59553: ML_file "~~/test/Pure/PIDE/xml.ML" wneuper@59553: ML \"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: wneuper@59553: section \test ML Code of isac\ wneuper@59600: subsection \basic code first\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\ wneuper@59594: ML_file "CalcElements/libraryC.sml" walther@59633: ML_file "CalcElements/rule.sml" wneuper@59594: ML_file "CalcElements/calcelems.sml" walther@59633: ML_file "CalcElements/termC.sml" walther@59633: ML_file "CalcElements/contextC.sml" walther@59659: ML_file "CalcElements/environment.sml" walther@59633: ML_file "CalcElements/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59553: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) wneuper@59553: ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) walther@59633: ML_file "ProgLang/listC.sml" walther@59633: ML_file "ProgLang/prog_expr.sml" walther@59633: ML_file "ProgLang/program.sml" walther@59633: ML_file "ProgLang/prog_tac.sml" walther@59763: ML_file "ProgLang/tactical.sml" walther@59633: ML_file "ProgLang/auto_prog.sml" wneuper@59553: ML_file "ProgLang/rewrite.sml" walther@59623: ML_file "ProgLang/tools.sml" wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59553: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) wneuper@59600: wneuper@59600: subsection \basic functionality on simple example first\ wneuper@59553: ML_file "Minisubpbl/000-comments.sml" wneuper@59553: ML_file "Minisubpbl/100-init-rootpbl.sml" wneuper@59553: ML_file "Minisubpbl/150-add-given.sml" wneuper@59553: ML_file "Minisubpbl/200-start-method.sml" wneuper@59553: ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml" walther@59722: ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/300-init-subpbl.sml" wneuper@59553: ML_file "Minisubpbl/400-start-meth-subpbl.sml" wneuper@59553: ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml" walther@59722: ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/490-nxt-Check_Postcond.sml" wneuper@59553: ML_file "Minisubpbl/500-met-sub-to-root.sml" wneuper@59553: ML_file "Minisubpbl/530-error-Check_Elementwise.sml" wneuper@59553: ML_file "Minisubpbl/600-postcond.sml" wneuper@59553: ML_file "Minisubpbl/700-interSteps.sml" walther@59722: ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" walther@59686: ML_file "Minisubpbl/790-complete.sml" wneuper@59600: wneuper@59600: subsection \further functionality alongside batch build sequence\ walther@59674: ML_file "MathEngBasic/model.sml" walther@59674: ML_file "MathEngBasic/mstools.sml" walther@59674: ML_file "MathEngBasic/specification-elems.sml" walther@59728: ML_file "MathEngBasic/tactic.sml" walther@59674: ML_file "MathEngBasic/ctree.sml" (*!...!see(25)*) walther@59763: wneuper@59594: ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *) wneuper@59553: ML \(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\ wneuper@59594: ML_file "Specify/generate.sml" wneuper@59594: ML_file "Specify/calchead.sml" wneuper@59594: ML_file "Specify/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *) walther@59763: ML_file "Specify/specify.sml" walther@59763: ML_file "Specify/step-specify.sml" wneuper@59600: wneuper@59553: ML_file "Interpret/rewtools.sml" wneuper@59553: ML_file "Interpret/script.sml" wneuper@59561: ML_file "Interpret/inform.sml" wneuper@59561: ML_file "Interpret/lucas-interpreter.sml" walther@59751: ML_file "Interpret/step-solve.sml" walther@59751: wneuper@59600: ML_file "MathEngine/solve.sml" walther@59763: ML_file "MathEngine/step.sml" wneuper@59600: ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) wneuper@59600: ML_file "MathEngine/messages.sml" wneuper@59600: ML_file "MathEngine/states.sml" wneuper@59600: wneuper@59600: ML_file "BridgeLibisabelle/mathml.sml" (*part.*) wneuper@59600: ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*) wneuper@59600: ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*) wneuper@59600: ML_file "BridgeLibisabelle/thy-hierarchy.sml" wneuper@59600: ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) wneuper@59600: ML_file "BridgeLibisabelle/interface.sml" wneuper@59553: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: wneuper@59553: ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) wneuper@59600: wneuper@59553: ML_file "Knowledge/delete.sml" wneuper@59553: ML_file "Knowledge/descript.sml" wneuper@59553: ML_file "Knowledge/atools.sml" wneuper@59553: ML_file "Knowledge/simplify.sml" wneuper@59553: ML_file "Knowledge/poly.sml" wneuper@59553: ML_file "Knowledge/gcd_poly_ml.sml" wneuper@59553: ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) wneuper@59556: (*ML_file "Knowledge/rational.sml" Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/equation.sml" wneuper@59553: ML_file "Knowledge/root.sml" wneuper@59553: ML_file "Knowledge/lineq.sml" wneuper@59553: (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) walther@59628: (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/rootrat.sml" wneuper@59553: ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) walther@59628: (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) walther@59628: ML_file "Knowledge/polyeq-1.sml" walther@59636: (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*) wneuper@59553: (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) wneuper@59553: ML_file "Knowledge/calculus.sml" wneuper@59553: ML_file "Knowledge/trig.sml" wneuper@59553: (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) wneuper@59553: ML_file "Knowledge/diff.sml" wneuper@59553: ML_file "Knowledge/integrate.sml" wneuper@59553: ML_file "Knowledge/eqsystem.sml" wneuper@59553: ML_file "Knowledge/test.sml" wneuper@59553: ML_file "Knowledge/polyminus.sml" wneuper@59553: ML_file "Knowledge/vect.sml" wneuper@59553: ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *) walther@59623: ML_file "Knowledge/biegelinie-1.sml" walther@59628: (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*) walther@59628: (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*) walther@59628: (*ML_file "Knowledge/biegelinie-4.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/algein.sml" wneuper@59553: ML_file "Knowledge/diophanteq.sml" walther@59628: (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/inssort.sml" wneuper@59553: ML_file "Knowledge/isac.sml" wneuper@59553: ML_file "Knowledge/build_thydata.sml" wneuper@59600: walther@59617: section \further tests additional to src/.. files\ wneuper@59600: ML_file "BridgeLibisabelle/use-cases.sml" wneuper@59553: ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" wneuper@59553: ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" wneuper@59600: wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59561: ML \ wneuper@59561: \ ML \ wneuper@59561: \ ML \ wneuper@59561: \ wneuper@59553: wneuper@59553: section \history of tests\ wneuper@59553: text \ wneuper@59553: Systematic regression tests have been introduced to isac development in 2003. wneuper@59553: Sanity of the regression tests suffers from updates following Isabelle development, wneuper@59553: which mostly exceeded the resources available in isac's development. wneuper@59553: wneuper@59553: The survey below shall support to efficiently use the tests for isac wneuper@59553: on different Isabelle versions. Conclusion in most cases will be: wneuper@59553: wneuper@59553: !!! Use most recent tests or go back to the old notebook wneuper@59553: with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! wneuper@59553: \ wneuper@59553: wneuper@59553: wneuper@59553: subsection \isac on Isabelle2017\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: * Add further signatures, separate structures and cleanup respective files. wneuper@59553: * Show feasibility of moving Isac programs to partial_function, i.e. to the function package. wneuper@59553: * Clean theory dependencies. wneuper@59553: * Start preparing shift from isac-java to Isabelle/jEdit. wneuper@59553: \ wneuper@59553: subsubsection \State of tests: unchanged\ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: last changeset with Test_Isac 925fef0f4c81 wneuper@59553: first changeset with Test_Isac bbb414976dfe wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2015\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang). wneuper@59553: This complicates Test_Isac, see "Prepare running tests" above. wneuper@59553: * Remove TTY interface. wneuper@59553: * Re-activate insertion sort. wneuper@59553: \ wneuper@59553: subsubsection \State of tests: unchanged\ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: last changeset with Test_Isac 2f1b2854927a wneuper@59553: first changeset with Test_Isac ??? wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2014\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: migration from "isabelle tty" --> libisabelle wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2013-2\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: reactivated context_thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: TODO wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: TODO wneuper@59553: : wneuper@59553: : isac on Isablle2013-2 wneuper@59553: : wneuper@59553: Changeset: 55318 (03826ceb24da) merged wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2013-12-12 14:27:37 +0100 (7 minutes) wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2013-1\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: Isabelle2013-1 was replaced within a few weeks due to problems with the document model; wneuper@59553: no significant development steps for ISAC. wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: See points in subsection "isac on Isabelle2011", "State of tests". wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2013-12-03 18:13:31 +0100 (8 days) wneuper@59553: : wneuper@59553: : isac on Isablle2013-1 wneuper@59553: : wneuper@59553: Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2013-11-21 18:12:17 +0100 (2 weeks) wneuper@59553: wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2013\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: # Oct.13: replaced "axioms" by "axiomatization" wneuper@59553: # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref wneuper@59553: # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into wneuper@59553: simplification of multivariate rationals (without improving the rulesets involved). wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: Is standard now; this subsection will be discontinued under Isabelle2013-1 wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: See points in subsection "isac on Isabelle2011", "State of tests". wneuper@59553: # re-activated listC.sml wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref" wneuper@59553: User: Mathias Lehnfeld wneuper@59553: Date: Tue Nov 19 22:23:30 2013 +0000 wneuper@59553: : wneuper@59553: : isac on Isablle2013 wneuper@59553: : wneuper@59553: Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013 wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2013-07-15 08:28:50 +0200 (4 weeks) wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2012\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: isac on Isabelle2012 is considered just a transitional stage wneuper@59553: within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; wneuper@59553: For considerations on the transition see wneuper@59553: ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..". wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: $ cd /usr/local/isabisac12/ wneuper@59553: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: At least the tests from isac on Isabelle2011 run again. wneuper@59553: However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling wneuper@59553: in parallel with evaluation. wneuper@59553: wneuper@59553: Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant) wneuper@59553: yields 69 hits, some of which were already present before Isabelle2002-->2009-2 wneuper@59553: (i.e. on the old notebook from 2002). wneuper@59553: wneuper@59553: Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin: wneuper@59553: # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy wneuper@59553: # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002 wneuper@59553: # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002 wneuper@59553: Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml. wneuper@59553: wneuper@59553: Some tests have been re-activated (e.g. error patterns, fill patterns). wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012 wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2013-07-11 16:58:31 +0200 (4 weeks) wneuper@59553: : wneuper@59553: : isac on Isablle2012 wneuper@59553: : wneuper@59553: Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012 wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2012-09-24 18:35:13 +0200 (8 months) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 48756 (7443906996a8) merged wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2012-09-24 18:15:49 +0200 (8 months) wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2011\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: isac's mathematics engine has been extended by two developments: wneuper@59553: (1) Isabelle's contexts were introduced by Mathias Lehnfeld wneuper@59553: (2) Z_Transform was introduced by Jan Rocnik, which revealed wneuper@59553: further errors introduced by (1). wneuper@59553: (3) "error patterns" were introduced by Gabriella Daroczy wneuper@59553: Regressions tests have been added for all of these. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: $ cd /usr/local/isabisac11/ wneuper@59553: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*) wneuper@59553: and sometimes give reasons for failing tests. wneuper@59553: (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable wneuper@59553: work, some of which couldn't be revised (and renamed) by WN and thus survived some time. wneuper@59553: wneuper@59553: The most signification tests (in particular Frontend/interface.sml) run, wneuper@59553: however, many "error in kernel" are not caught by an exception. wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: After the changeset below Test_Isac worked with check_unsynchronized_ref (): wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2012-08-06 10:38:11 +0200 (11 months) wneuper@59553: wneuper@59553: wneuper@59553: The list below records TODOs while producing an ISAC kernel for wneuper@59553: gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING wneuper@59553: (so to be resumed with Isabelle2013-1): wneuper@59553: ############## WNxxxxxx.TODO can be found in sources ############## wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111013.TODO: lots of cleanup/removal in test/../Test.thy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111013.TODO: remove concept around "fun init_form", lots of troubles with wneuper@59553: this special case (see) --- why not nxt = Model_Problem here ? --- wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/ wneuper@59553: ... FIRST redesign wneuper@59553: # simplify_* , *_simp_* wneuper@59553: # norm_* wneuper@59553: # calc_* , calculate_* ... require iteration over all rls ... wneuper@59553: ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE ! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120314 changeset a393bb9f5e9f drops root equations. wneuper@59553: see test/Tools/isac/Knowledge/rootrateq.sml wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO changeset 977788dfed26 dropped rateq: wneuper@59553: # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002 wneuper@59553: # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...: wneuper@59553: investigation Check_elementwise stopped due to too much effort finding out, wneuper@59553: why Check_elementwise worked in 2002 in spite of the error. wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO found by test --- interSteps for Schalk 299a --- that wneuper@59553: NO test with 'interSteps' is checked properly (with exn on changed behaviour) wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has wneuper@59553: a newly outcommented test where rewrite_set_ make_polynomial --> NONE wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120320.TODO check-improve rlsthmsNOTisac: wneuper@59553: DONE make test --- old compute rlsthmsNOTisac by eq_thmI' wneuper@59553: DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy wneuper@59553: FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab wneuper@59553: # mark twice thms (in isac + (later) in Isabelle) in Isac.thy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120320.TODO rlsthmsNOTisac: replace twice thms ^ wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test wneuper@59553: --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac. wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO rearrange theories: wneuper@59553: Knowledge wneuper@59553: : walther@59603: Prog_Expr.thy wneuper@59553: ///Descript.thy --> ProgLang walther@59603: Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*) wneuper@59553: ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy wneuper@59553: Interpret.thy are generated (simplifies xml structure for theories) wneuper@59585: Program.thy wneuper@59553: Tools.thy wneuper@59553: ListC.thy <--- first_Proglang_thy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify wneuper@59553: EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)" wneuper@59553: broken during work on thy-hierarchy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see wneuper@59553: test --- the_hier (get_thes ()) (collect_thydata ())--- wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_ wneuper@59553: !!add mutual crossreferences to ?fun headline??? where the same has to be done: wneuper@59553: !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120409.TODO replace "op mem" (2002) with member (2011) ... wneuper@59553: ... an exercise interesting for beginners ! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120411 scanning html representation of newly generated knowledge: wneuper@59553: * thy: wneuper@59553: ** Theorems: only "Proof of the theorem" (correct!) wneuper@59553: and "(c) isac-team (math-autor)" wneuper@59553: ** Rulesets: only "Identifier:///" wneuper@59553: and "(c) isac-team (math-autor)" wneuper@59553: ** IsacKnowledge: link to dependency graph (which needs to be created first) wneuper@59553: ** IsacScripts --> ProgramLanguage wneuper@59553: *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen wneuper@59553: wneuper@59553: * pbl: OK !?! wneuper@59553: * met: OK !?! wneuper@59553: * exp: wneuper@59553: ** Z-Transform is missing !!! wneuper@59553: ** type-constraints !!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120417: merging xmldata revealed: wneuper@59553: ..............NEWLY generated:........................................ wneuper@59553: wneuper@59553: thy_isab_Fun-thm-o_apply wneuper@59553: wneuper@59553: Isabelle wneuper@59553: Fun wneuper@59553: Theorems wneuper@59553: o_apply wneuper@59553: wneuper@59553: wneuper@59553: (?f o ?g) ?x = ?f (?g ?x) wneuper@59553: wneuper@59553: wneuper@59553: Proof of the theorem wneuper@59553: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Isabelle team, TU Munich wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: ..............OLD FORMAT:............................................. wneuper@59553: wneuper@59553: thy_isab_Fun-thm-o_apply wneuper@59553: wneuper@59553: Isabelle wneuper@59553: Fun wneuper@59553: Theorems wneuper@59553: o_apply wneuper@59553: wneuper@59553: wneuper@59553: o_apply wneuper@59553: wneuper@59553: (?f o ?g) ?x = ?f (?g ?x) wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Proof of the theorem wneuper@59553: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Isabelle team, TU Munich wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: isac development was done between these changesets: wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2012-09-24 16:39:30 +0200 (8 months) wneuper@59553: : wneuper@59553: : isac on Isablle2011 wneuper@59553: : wneuper@59553: Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011 wneuper@59553: Branch: decompose-isar wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2011-02-25 13:04:56 +0100 (2011-02-25) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2009-2\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg. wneuper@59553: The update was painful (bridging 7 years of Isabelle development) and cut short wneuper@59553: due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and wneuper@59553: going on to Isabelle2011 although most of the tests did not run. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: WN131021 this is broken by installation of Isabelle2011/12/13, wneuper@59553: because all these write their binaries to ~/.isabelle/heaps/.. wneuper@59553: wneuper@59553: $ cd /usr/local/isabisac09-2/ wneuper@59553: $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy wneuper@59553: NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!! wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: Most tests are broken by the update from Isabelle2002 to Isabelle2009-2. wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: isac development was done between these changesets: wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 38115 (940a5feea094) Little improvements of isac-plugin wneuper@59553: Branch: decompose-isar wneuper@59553: User: Marco Steger wneuper@59553: Date: 2011-02-06 18:30:28 +0100 (2011-02-06) wneuper@59553: : wneuper@59553: : isac on Isablle2009-2 wneuper@59553: : wneuper@59553: Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 wneuper@59553: Branch: isac-from-Isabelle2009-2 wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2010-07-21 09:59:35 +0200 (2010-07-21) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2002\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern") wneuper@59553: of isac's mathematics engine has been implemented. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: All tests work on an old notebook (the right PolyML coudn't be upgraded to more wneuper@59553: recent Linux versions) wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS; wneuper@59553: see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial. wneuper@59553: \ wneuper@59553: wneuper@59553: end wneuper@59553: (*========== inhibit exn 130719 Isabelle2013 =================================== wneuper@59553: ============ inhibit exn 130719 Isabelle2013 =================================*) wneuper@59553: wneuper@59553: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. wneuper@59553: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) wneuper@59553: