Walther@60424: (* 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: wenzelm@60192: $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC wneuper@59553: plus wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality walther@59935: walther@59935: Note, that only the first error in a file is shown here. 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: 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@59964: \\******************* 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 ..*) walther@59997: (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one walther@59997: and find out, which ML_file or *.thy causes an error (might be ONLY one). walther@59997: Also backup files (#* ) recognised by jEdit cause this trouble *) wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) walther@60317: (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*) walther@60387: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics" walther@60317: (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*) wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo" wneuper@59553: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" wneuper@59553: ADDTESTS/------------------------------------------- see end of tests *) walther@60317: (*/~~~ these work directly from Pure, but create problems here .. wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *) walther@60317: \~~~ .. these work independently, but create problems here *) wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer" wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) walther@60317: (** ) wneuper@59553: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) wenzelm@60192: (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*) wenzelm@60192: (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*) wneuper@59556: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) walther@60317: ( **) Walther@60491: "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example" wneuper@59553: wneuper@59553: begin wneuper@59553: wenzelm@60240: declare [[ML_print_depth = 20]] wenzelm@60240: walther@59628: ML \open ML_System\ wneuper@59553: ML \ wneuper@59553: open Kernel; walther@59814: open Math_Engine; walther@59814: open Test_Code; CalcTreeTEST; walther@59848: open LItool; arguments_from_model; walther@59817: open Sub_Problem; walther@59823: open Fetch_Tacs; walther@59814: open Step walther@59659: open Env; walther@59814: open LI; scan_dn; walther@59617: open Istate; walther@59909: open Error_Pattern; walther@59909: open Error_Pattern_Def; walther@59977: open Specification; 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; walther@59971: open Specify; walther@59976: open Specify; walther@59763: open Step_Specify; walther@59749: open Step_Solve; walther@59763: open Step; wneuper@59553: open Solve; (* NONE *) wneuper@59577: open ContextC; transfer_asms_from_to; walther@59814: open Tactic; (* NONE *) walther@60126: open I_Model; walther@60126: open O_Model; walther@60126: open P_Model; (* NONE *) walther@59872: open Rewrite; walther@59878: open Eval; get_pair; wneuper@59553: open TermC; atomt; walther@59858: open Rule; walther@59878: open Rule_Set; Sequence; walther@59919: open Eval_Def walther@59854: open ThyC walther@59865: open ThmC_Def walther@59858: open ThmC walther@59857: open Rewrite_Ord walther@59861: open UnparseC wenzelm@60223: \ wneuper@59553: wneuper@59553: ML \ walther@59659: "~~~~~ fun xxx , args:"; val () = (); walther@59659: "~~~~~ and xxx , args:"; val () = (); walther@59814: "~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); walther@60262: (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); walther@59659: "xx" walther@60329: ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) walther@60329: \ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) walther@59723: \ ML \ walther@60329: \ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) walther@59723: \ walther@59723: ML \ walther@59723: \ ML \ wneuper@59553: \ ML \ walther@59851: \ ML \ walther@59851: \ 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: section \trials with Isabelle's functions\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ Walther@60424: ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_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 %%%%%%%%%%%%%%%%%%%";\ walther@60413: ML_file "BaseDefinitions/base-definitions.sml" walther@59866: ML_file "BaseDefinitions/libraryC.sml" walther@59866: ML_file "BaseDefinitions/rule-def.sml" walther@59919: ML_file "BaseDefinitions/eval-def.sml" walther@59866: ML_file "BaseDefinitions/rewrite-order.sml" walther@59866: ML_file "BaseDefinitions/theoryC.sml" walther@59866: ML_file "BaseDefinitions/rule.sml" walther@59866: ML_file "BaseDefinitions/thmC-def.sml" walther@59866: ML_file "BaseDefinitions/error-fill-def.sml" walther@59866: ML_file "BaseDefinitions/rule-set.sml" walther@59892: ML_file "BaseDefinitions/check-unique.sml" walther@59932: (*called by Know_Store..*) walther@59866: ML_file "BaseDefinitions/calcelems.sml" walther@59866: ML_file "BaseDefinitions/termC.sml" walther@59912: ML_file "BaseDefinitions/substitution.sml" Walther@60424: ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*) walther@59866: ML_file "BaseDefinitions/environment.sml" Walther@60424: (**)ML_file "BaseDefinitions/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 --------------------------------*) walther@59932: walther@60317: ML_file "ProgLang/calculate.sml" walther@59964: ML_file "ProgLang/evaluate.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@60326: ML_file "ProgLang/auto_prog.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" walther@59781: ML_file "Minisubpbl/200-start-method-NEXT_STEP.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" walther@59781: ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/600-postcond.sml" wneuper@59553: ML_file "Minisubpbl/700-interSteps.sml" walther@59820: ML_file "Minisubpbl/710-interSteps-short.sml" walther@59836: ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" walther@59686: ML_file "Minisubpbl/790-complete.sml" walther@60340: ML_file "Minisubpbl/800-append-on-Frm.sml" wneuper@59600: wneuper@59600: subsection \further functionality alongside batch build sequence\ walther@59865: ML_file "MathEngBasic/thmC.sml" walther@60389: ML_file "MathEngBasic/rewrite.sml" walther@59728: ML_file "MathEngBasic/tactic.sml" walther@60389: ML_file "MathEngBasic/ctree.sml" walther@59774: ML_file "MathEngBasic/calculation.sml" walther@59763: walther@59996: ML_file "Specify/formalise.sml" walther@59952: ML_file "Specify/o-model.sml" walther@59957: ML_file "Specify/i-model.sml" walther@59996: ML_file "Specify/pre-conditions.sml" walther@59996: ML_file "Specify/p-model.sml" walther@59985: ML_file "Specify/m-match.sml" walther@59967: ML_file "Specify/refine.sml" (* requires setup from refine.thy *) walther@59996: ML_file "Specify/test-out.sml" walther@59996: ML_file "Specify/specify-step.sml" walther@59996: ML_file "Specify/specification.sml" walther@59996: ML_file "Specify/cas-command.sml" walther@59996: ML_file "Specify/p-spec.sml" walther@59996: ML_file "Specify/specify.sml" walther@59800: ML_file "Specify/step-specify.sml" walther@59813: walther@59860: ML_file "Interpret/istate.sml" walther@59817: ML_file "Interpret/sub-problem.sml" walther@60389: ML_file "Interpret/error-pattern.sml" walther@59790: ML_file "Interpret/li-tool.sml" walther@60340: ML_file "Interpret/lucas-interpreter.sml" walther@59751: ML_file "Interpret/step-solve.sml" walther@59751: walther@60326: ML_file "MathEngine/me-misc.sml" walther@59823: ML_file "MathEngine/fetch-tactics.sml" walther@60326: ML_file "MathEngine/solve.sml" walther@59763: ML_file "MathEngine/step.sml" walther@60340: ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) walther@60326: ML_file "MathEngine/messages.sml" wneuper@59600: ML_file "MathEngine/states.sml" wneuper@59600: walther@59917: ML_file "BridgeLibisabelle/thy-present.sml" wneuper@59600: ML_file "BridgeLibisabelle/mathml.sml" (*part.*) walther@60277: ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" wneuper@59600: ML_file "BridgeLibisabelle/thy-hierarchy.sml" Walther@60424: ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) walther@60389: ML_file "BridgeLibisabelle/interface.sml" walther@60044: ML_file "BridgeJEdit/parseC.sml" walther@60146: ML_file "BridgeJEdit/preliminary.sml" Walther@60465: ML_file "BridgeJEdit/vscode-example.sml" walther@60044: wneuper@59553: ML_file "Knowledge/delete.sml" wneuper@59553: ML_file "Knowledge/descript.sml" wneuper@59553: ML_file "Knowledge/simplify.sml" walther@60340: ML_file "Knowledge/poly-1.sml" walther@60329: (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/gcd_poly_ml.sml" walther@60329: ML_file "Knowledge/rational-1.sml" walther@60329: (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) Walther@60465: ML_file "Knowledge/equation.sml" walther@60384: ML_file "Knowledge/root.sml" wneuper@59553: ML_file "Knowledge/lineq.sml" walther@60318: 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*) walther@60389: 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@60393: ML_file "Knowledge/polyeq-1.sml" walther@60393: (*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*) walther@60350: ML_file "Knowledge/diff.sml" walther@60350: ML_file "Knowledge/integrate.sml" walther@60347: ML_file "Knowledge/eqsystem-1.sml" walther@60395: ML_file "Knowledge/eqsystem-2.sml" walther@59996: ML_file "Knowledge/test.sml" wneuper@59553: ML_file "Knowledge/polyminus.sml" wneuper@59553: ML_file "Knowledge/vect.sml" Walther@60458: ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *) walther@60396: 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@60398: ML_file "Knowledge/biegelinie-4.sml" walther@60326: 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@59814: ML_file "Test_Code/test-code.sml" walther@59814: walther@59617: section \further tests additional to src/.. files\ walther@60399: ML_file "BridgeLibisabelle/use-cases.sml" wneuper@59600: wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ walther@60262: ML \ walther@60262: \ ML \ wneuper@59561: \ ML \ walther@59804: \ ML \ walther@59804: \ 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: Walther@60424: 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: : Walther@60424: : isac on Isablle2013-2 wneuper@59553: : wneuper@59553: Changeset: 55318 (03826ceb24da) merged wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-12-12 14:27:37 +0100 (7 minutes) wneuper@59553: \ wneuper@59553: Walther@60424: subsection \isac on Isabelle2013-1\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ Walther@60424: 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 Walther@60424: Date: 2013-12-03 18:13:31 +0100 (8 days) wneuper@59553: : Walther@60424: : isac on Isablle2013-1 wneuper@59553: : Walther@60424: Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect wneuper@59553: User: Walther Neuper Walther@60424: 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 \ Walther@60424: 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 Walther@60424: 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 wenzelm@60192: $ISABELLE_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) Walther@60424: 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 Walther@60424: # === 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 Walther@60424: 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 Walther@60424: Date: 2012-09-24 18:35:13 +0200 (8 months) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 48756 (7443906996a8) merged wneuper@59553: User: Walther Neuper Walther@60424: 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 Walther@60424: (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: -------------------------------------------------------------------------------- walther@59845: WN111013.TODO: remove concept around "fun implicit_take", 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 Walther@60424: # 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' Walther@60424: 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: -------------------------------------------------------------------------------- Walther@60424: 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 walther@60125: ///Input_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: 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 Walther@60424: 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 Walther@60424: Date: 2011-02-25 13:04:56 +0100 (2011-02-25) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: \ wneuper@59553: Walther@60424: 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: Walther@60424: $ 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 \ Walther@60424: 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: : Walther@60424: : isac on Isablle2009-2 wneuper@59553: : Walther@60424: Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 Walther@60424: Branch: isac-from-Isabelle2009-2 wneuper@59553: User: Walther Neuper Walther@60424: 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: