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: wenzelm@60192: $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC neuper@52101: plus wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality walther@59957: walther@59957: Note, that only the first error in a file is shown here. neuper@41943: *) neuper@41943: walther@59623: section \Notes on running tests\ walther@59623: subsection \Switch between running tests and updating code\ wneuper@59258: 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@59323: 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@59323: walther@59967: \\******************* 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@59258: \ wneuper@59258: 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: walther@59623: theory Test_Isac walther@59623: imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) walther@60028: (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one walther@60028: and find out, which ML_file or *.thy causes an error (might be ONLY one). walther@60028: Also backup files (#* ) recognised by jEdit cause this trouble *) wneuper@59465: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) Walther@60424: (* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*) Walther@60424: (**)"$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" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" 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@59144: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" wneuper@59144: ADDTESTS/------------------------------------------- see end of tests *) Walther@60424: (*/~~~ 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@60424: \~~~ .. these work independently, but create problems here *) wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers" Walther@60424: (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer" wneuper@59364: (*/---------------------- 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@60424: (**) wneuper@59364: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) Walther@60519: "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*) Walther@60519: "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*) wneuper@59364: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) Walther@60424: (**) Walther@60624: "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example" neuper@52168: neuper@41943: begin s1210629013@55442: Walther@60640: declare [[ML_print_depth = 20]] (*otherwise buffer overflow*) Walther@60424: walther@59659: ML \open ML_System\ wneuper@59472: ML \ wneuper@59261: open Kernel; walther@59814: open Math_Engine; Walther@60571: open Test_Code; Test_Code.init_calc @{context}; 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; wneuper@59600: open Istate; walther@59909: open Error_Pattern; walther@59909: open Error_Pattern_Def; walther@59977: open Specification; wneuper@59276: open Ctree; append_problem; walther@59722: 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; walther@59617: open Input_Descript; walther@59971: open Specify; walther@59976: open Specify; walther@59763: open Step_Specify; walther@59763: open Step_Solve; walther@59763: open Step; wneuper@59316: 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@59892: open Rewrite; walther@59878: open Eval; get_pair; Walther@60650: open TermC; walther@59858: open Rule; walther@59892: open Rule_Set; Sequence; walther@59919: open Eval_Def walther@59858: open ThyC walther@59865: open ThmC_Def walther@59858: open ThmC walther@59858: open Rewrite_Ord Walther@60608: open UnparseC; Walther@60608: Walther@60608: Know_Store.set_ref_last_thy @{theory}; Walther@60608: (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*) wenzelm@60223: \ wneuper@59366: wneuper@59462: ML \ walther@59674: "~~~~~ fun xxx , args:"; val () = (); walther@59674: "~~~~~ and xxx , args:"; val () = (); Walther@60424: "~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); Walther@60578: "~~~~~ continue fun xxx"; val () = (); Walther@60424: (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); walther@59674: "xx" Walther@60629: ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**) Walther@60567: \ ML \ (*//----------- adhoc inserted n ----------------------------------------------------\\*) Walther@60567: (*//----------------- adhoc inserted n ----------------------------------------------------\\*) Walther@60567: (*\\------------------ adhoc inserted n ----------------------------------------------------//*) Walther@60567: \ ML \ (*\\----------- adhoc inserted n ----------------------------------------------------//*) Walther@60578: Walther@60578: \ ML \ (*//----------- step into XXXXX -----------------------------------------------------\\*) Walther@60578: (*//------------------ step into XXXXX -----------------------------------------------------\\*) Walther@60629: (*keep for continuing YYYYY*) Walther@60578: \ ML \ (*------------- continuing XXXXX ------------------------------------------------------*) Walther@60578: (*-------------------- continuing XXXXX ------------------------------------------------------*) Walther@60578: (*kept for continuing XXXXX*) Walther@60578: (*-------------------- stop step into XXXXX --------------------------------------------------*) Walther@60578: \ ML \ (*------------- stop step into XXXXX --------------------------------------------------*) Walther@60578: (*\\------------------ step into XXXXX -----------------------------------------------------//*) Walther@60578: \ ML \ (*\\----------- step into XXXXX -----------------------------------------------------//*) Walther@60578: Walther@60578: (*/------------------- check entry to XXXXX -------------------------------------------------\*) Walther@60578: (*\------------------- check entry to XXXXX -------------------------------------------------/*) Walther@60578: (*/------------------- check within XXXXX ---------------------------------------------------\*) Walther@60578: (*\------------------- check within XXXXX ---------------------------------------------------/*) Walther@60578: (*/------------------- check result of XXXXX ------------------------------------------------\*) Walther@60578: (*\------------------- check result of XXXXX ------------------------------------------------/*) Walther@60578: (* final test ... ----------------------------------------------------------------------------*) Walther@60578: Walther@60578: \ ML \ (*//----------- inserted hidden code ------------------------------------------------\\*) Walther@60578: (*//------------------ inserted hidden code ------------------------------------------------\\*) Walther@60578: (*\\------------------ inserted hidden code ------------------------------------------------//*) Walther@60578: \ ML \ (*\\----------- inserted hidden code ------------------------------------------------//*) Walther@60578: Walther@60578: \ ML \ (*//----------- build new fun XXXXX -------------------------------------------------\\*) Walther@60578: (*//------------------ build new fun XXXXX -------------------------------------------------\\*) Walther@60578: (*\\------------------ build new fun XXXXX -------------------------------------------------//*) Walther@60578: \ ML \ (*\\----------- build new fun XXXXX -------------------------------------------------//*) walther@59763: \ walther@59763: ML \ walther@59763: \ ML \ wneuper@59462: \ ML \ walther@59858: \ ML \ walther@59858: \ ML \ wneuper@59462: \ wneuper@59356: wneuper@59472: ML \ wneuper@59248: (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); wneuper@59472: \ s1210629013@55442: wneuper@59472: section \trials with Isabelle's functions\ wneuper@59472: ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ wenzelm@60217: 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@59472: ML \"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\ neuper@52119: wneuper@59472: section \test ML Code of isac\ wneuper@59600: subsection \basic code first\ wneuper@59472: ML \"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\ Walther@60424: 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@60624: ML_file "BaseDefinitions/model-pattern.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@59957: (*called by Know_Store..*) walther@59866: ML_file "BaseDefinitions/calcelems.sml" walther@59866: ML_file "BaseDefinitions/termC.sml" walther@59917: ML_file "BaseDefinitions/substitution.sml" Walther@60558: ML_file "BaseDefinitions/contextC.sml"(*sometimes needs separation into ML blocks for evaluation*) walther@59866: ML_file "BaseDefinitions/environment.sml" Walther@60424: (** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) wneuper@59356: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59388: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) walther@59957: Walther@60519: ML_file "ProgLang/calculate.sml" walther@59967: ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *) walther@59659: ML_file "ProgLang/listC.sml" walther@59659: ML_file "ProgLang/prog_expr.sml" walther@59659: ML_file "ProgLang/program.sml" walther@59659: ML_file "ProgLang/prog_tac.sml" walther@59659: ML_file "ProgLang/tactical.sml" walther@59659: ML_file "ProgLang/auto_prog.sml" wneuper@59362: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59366: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) wneuper@59600: wneuper@59600: subsection \basic functionality on simple example first\ neuper@52065: ML_file "Minisubpbl/000-comments.sml" neuper@52065: ML_file "Minisubpbl/100-init-rootpbl.sml" Walther@60578: ML_file "Minisubpbl/150a-add-given-Maximum.sml" Walther@60592: ML_file "Minisubpbl/150-add-given-Equation.sml" walther@59781: ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml" neuper@52065: ML_file "Minisubpbl/200-start-method.sml" wneuper@59411: ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml" walther@59722: ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml" neuper@52065: ML_file "Minisubpbl/300-init-subpbl.sml" neuper@52065: ML_file "Minisubpbl/400-start-meth-subpbl.sml" wneuper@59492: ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml" walther@59722: ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.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" walther@59781: ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml" neuper@52065: ML_file "Minisubpbl/600-postcond.sml" wneuper@59493: ML_file "Minisubpbl/700-interSteps.sml" Walther@60649: ML_file "Minisubpbl/710-interSteps-short.sml" walther@59722: ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" walther@59686: ML_file "Minisubpbl/790-complete.sml" walther@59817: 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@60624: ML_file "MathEngBasic/problem.sml" walther@59865: ML_file "MathEngBasic/rewrite.sml" walther@59763: ML_file "MathEngBasic/tactic.sml" Walther@60624: ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*) walther@59817: ML_file "MathEngBasic/calculation.sml" walther@59674: walther@59996: ML_file "Specify/formalise.sml" walther@59957: 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@60609: ML_file "Specify/sub-problem.sml" walther@59817: ML_file "Specify/step-specify.sml" wneuper@59600: walther@59865: ML_file "Interpret/istate.sml" walther@59909: ML_file "Interpret/error-pattern.sml" walther@59817: ML_file "Interpret/li-tool.sml" wneuper@59561: ML_file "Interpret/lucas-interpreter.sml" walther@59763: ML_file "Interpret/step-solve.sml" wneuper@59600: walther@59996: ML_file "MathEngine/me-misc.sml" walther@59823: ML_file "MathEngine/fetch-tactics.sml" wneuper@59600: ML_file "MathEngine/solve.sml" walther@59763: ML_file "MathEngine/step.sml" Walther@60558: ML_file "MathEngine/mathengine-stateless.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.*) Walther@60519: ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" wneuper@59600: ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) wneuper@59600: ML_file "BridgeLibisabelle/interface.sml" Walther@60624: walther@60090: ML_file "BridgeJEdit/parseC.sml" Walther@60465: ML_file "BridgeJEdit/preliminary.sml" Walther@60465: ML_file "BridgeJEdit/vscode-example.sml" walther@60090: neuper@52065: ML_file "Knowledge/delete.sml" neuper@52065: ML_file "Knowledge/descript.sml" neuper@52065: ML_file "Knowledge/simplify.sml" Walther@60519: ML_file "Knowledge/poly-1.sml" Walther@60594: ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*) wneuper@59370: ML_file "Knowledge/gcd_poly_ml.sml" Walther@60424: ML_file "Knowledge/rational-1.sml" Walther@60424: ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*) 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 *) walther@59628: ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered----Test_Isac_Short*) wneuper@59370: ML_file "Knowledge/rootrat.sml" wneuper@59370: 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@59627: ML_file "Knowledge/polyeq-1.sml" walther@59628: ML_file "Knowledge/polyeq-2.sml" (*Test_Isac_Short*) 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" Walther@60424: ML_file "Knowledge/eqsystem-1.sml" Walther@60556: ML_file "Knowledge/eqsystem-1a.sml" Walther@60424: ML_file "Knowledge/eqsystem-2.sml" neuper@52065: ML_file "Knowledge/test.sml" neuper@52065: ML_file "Knowledge/polyminus.sml" neuper@52065: ML_file "Knowledge/vect.sml" Walther@60458: ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *) walther@59627: 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@60024: ML_file "Knowledge/biegelinie-4.sml" neuper@52065: ML_file "Knowledge/algein.sml" neuper@52065: ML_file "Knowledge/diophanteq.sml" walther@59628: (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*) wneuper@59232: ML_file "Knowledge/inssort.sml" neuper@52065: ML_file "Knowledge/isac.sml" wneuper@59600: walther@59817: ML_file "Test_Code/test-code.sml" walther@59817: walther@59617: section \further tests additional to src/.. files\ wneuper@59600: ML_file "BridgeLibisabelle/use-cases.sml" wneuper@59600: wneuper@59472: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59472: ML \"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59472: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59559: ML \ wneuper@59559: \ ML \ wneuper@59559: \ ML \ walther@59817: \ ML \ walther@59817: \ ML \ wneuper@59559: \ neuper@41943: wneuper@59472: section \history of tests\ wneuper@59472: 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. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! wneuper@59472: \ neuper@48895: wneuper@59323: wneuper@59472: subsection \isac on Isabelle2017\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: text \ wneuper@59449: * Add further signatures, separate structures and cleanup respective files. wneuper@59449: * Show feasibility of moving Isac programs to partial_function, i.e. to the function package. wneuper@59449: * Clean theory dependencies. wneuper@59449: * Start preparing shift from isac-java to Isabelle/jEdit. wneuper@59472: \ wneuper@59472: subsubsection \State of tests: unchanged\ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: text \ wneuper@59449: last changeset with Test_Isac 925fef0f4c81 wneuper@59449: first changeset with Test_Isac bbb414976dfe wneuper@59472: \ wneuper@59449: wneuper@59472: subsection \isac on Isabelle2015\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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@59472: \ wneuper@59472: subsubsection \State of tests: unchanged\ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: text \ wneuper@59323: last changeset with Test_Isac 2f1b2854927a wneuper@59323: first changeset with Test_Isac ??? wneuper@59472: \ wneuper@59323: wneuper@59472: subsection \isac on Isabelle2014\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: text \ wneuper@59120: migration from "isabelle tty" --> libisabelle wneuper@59472: \ wneuper@59120: wneuper@59472: subsection \isac on Isabelle2013-2\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: text \ wneuper@55500: reactivated context_thy wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: text \ neuper@55319: TODO wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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) wneuper@59472: \ neuper@55319: wneuper@59472: subsection \isac on Isabelle2013-1\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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. wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: text \ neuper@55284: See points in subsection "isac on Isabelle2011", "State of tests". wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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: wneuper@59472: \ neuper@55284: wneuper@59472: subsection \isac on Isabelle2013\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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). wneuper@59472: \ wneuper@59472: subsubsection \Run tests\ wneuper@59472: text \ neuper@52150: Is standard now; this subsection will be discontinued under Isabelle2013-1 wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: text \ neuper@52150: See points in subsection "isac on Isabelle2011", "State of tests". neuper@52150: # re-activated listC.sml wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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) wneuper@59472: \ neuper@48895: wneuper@59472: subsection \isac on Isabelle2012\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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 wenzelm@60192: $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..". wneuper@59472: \ wneuper@59472: subsubsection \Run tests\ wneuper@59472: 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 wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: 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). wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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) wneuper@59472: \ neuper@48895: wneuper@59472: subsection \isac on Isabelle2011\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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. wneuper@59472: \ wneuper@59472: subsubsection \Run tests\ wneuper@59472: 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 wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: 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: -------------------------------------------------------------------------------- walther@59845: WN111013.TODO: remove concept around "fun implicit_take", 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: : walther@59603: Prog_Expr.thy walther@60125: ///Input_Descript.thy --> ProgLang walther@59603: Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.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) wneuper@59585: Program.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: 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: -------------------------------------------------------------------------------- wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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: ------------------------------------------------------------------------------ wneuper@59472: \ neuper@48895: wneuper@59472: subsection \isac on Isabelle2009-2\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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. wneuper@59472: \ wneuper@59472: subsubsection \Run tests\ wneuper@59472: 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 !!! wneuper@59472: \ wneuper@59472: subsubsection \State of tests\ wneuper@59472: text \ neuper@48895: Most tests are broken by the update from Isabelle2002 to Isabelle2009-2. wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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: ------------------------------------------------------------------------------ wneuper@59472: \ neuper@48895: wneuper@59472: subsection \isac on Isabelle2002\ wneuper@59472: subsubsection \Summary of development\ wneuper@59472: 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. wneuper@59472: \ wneuper@59472: subsubsection \Run tests\ wneuper@59472: subsubsection \State of tests\ wneuper@59472: text \ neuper@48895: All tests work on an old notebook (the right PolyML coudn't be upgraded to more neuper@48895: recent Linux versions) wneuper@59472: \ wneuper@59472: subsubsection \Changesets of begin and end\ wneuper@59472: 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. wneuper@59472: \ 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: