Getting the theorem prover up and running fails part way through

[joey-coleman]

The following bug was originally reported on Sourceforge by *anonymous, 2013-09-11 17:28:05.902000:

I get this error message: Building Isabelle session failed (return code 1) Session Pure Session HOL (main) Session HOL-Library (main) Session Datatype_Order_Generator (AFP) Session Kleene_Algebra (AFP) Session HOL-UTP Session HOL-UTP-THY Session HOL-UTP-CML Building HOL-Library ... HOL-Library: theory Adhoc_Overloading HOL-Library: theory Lattice_Syntax HOL-Library: theory Preorder HOL-Library: theory Refute HOL-Library: theory AList HOL-Library: theory Bit HOL-Library: theory Boolean_Algebra HOL-Library: theory Char_nat HOL-Library: theory Code_Binary_Nat HOL-Library: theory Char_ord HOL-Library: theory Code_Char HOL-Library: theory Code_Natural HOL-Library: theory Code_Numeral_Types HOL-Library: theory Code_Integer HOL-Library: theory Code_Char_ord HOL-Library: theory Code_Char_chr HOL-Library: theory Continuity HOL-Library: theory Debug HOL-Library: theory Dlist HOL-Library: theory Efficient_Nat HOL-Library: theory IArray HOL-Library: theory DAList HOL-Library: theory Eval_Witness HOL-Library: theory Extended_Nat HOL-Library: theory Fraction_Field HOL-Library: theory FuncSet HOL-Library: theory Function_Algebras HOL-Library: theory Code_Target_Int HOL-Library: theory Code_Target_Nat HOL-Library: theory Function_Division HOL-Library: theory Indicator_Function HOL-Library: theory Infinite_Set HOL-Library: theory Kleene_Algebra HOL-Library: theory Code_Target_Numeral HOL-Library: theory LaTeXsugar HOL-Library: theory ListVector HOL-Library: theory List_lexord HOL-Library: theory Monad_Syntax HOL-Library: theory Multiset HOL-Library: theory Option_ord HOL-Library: theory Order_Relation HOL-Library: theory Zorn HOL-Library: theory Parallel HOL-Library: theory Diagonal_Subsequence HOL-Library: theory Nat_Bijection HOL-Library: theory Abstract_Rat HOL-Library: theory Binomial HOL-Library: theory Countable HOL-Library: theory Code_Real_Approx_By_Float HOL-Library: theory ContNotDenum HOL-Library: theory Formal_Power_Series HOL-Library: theory Countable_Set HOL-Library: theory FrechetDeriv HOL-Library: theory Lattice_Algebras HOL-Library: theory Inner_Product HOL-Library: theory OptionalSugar HOL-Library: theory Sum_of_Squares HOL-Library: theory Permutations HOL-Library: theory Permutation HOL-Library: theory Phantom_Type HOL-Library: theory Cardinality HOL-Library: theory Polynomial HOL-Library: theory Product_plus HOL-Library: theory Float HOL-Library: theory Product_Lattice HOL-Library: theory Finite_Lattice HOL-Library: theory FinFun HOL-Library: theory Numeral_Type HOL-Library: theory Type_Length HOL-Library: theory Fundamental_Theorem_Algebra HOL-Library: theory Poly_Deriv HOL-Library: theory Product_Vector HOL-Library: theory Quotient_Syntax HOL-Library: theory Quotient_Option HOL-Library: theory Quotient_Product HOL-Library: theory Convex HOL-Library: theory Mapping HOL-Library: theory Quotient_Set HOL-Library: theory Quotient_Sum HOL-Library: theory Quotient_List HOL-Library: theory Quotient_Type HOL-Library: theory AList_Mapping HOL-Library: theory RBT_Impl HOL-Library: theory Ramsey HOL-Library: theory Reflection HOL-Library: theory Saturated HOL-Library: theory Set_Algebras HOL-Library: theory State_Monad HOL-Library: theory Sublist HOL-Library: theory BigO HOL-Library: theory Sublist_Order HOL-Library: theory Transitive_Closure_Table HOL-Library: theory Univ_Poly HOL-Library: theory Wfrec HOL-Library: theory Old_Recdef HOL-Library: theory While_Combinator HOL-Library: theory RBT HOL-Library: theory RBT_Mapping HOL-Library: theory Library Skipping theories "Sum_of_Squares_Remote" (undefined ISABELLE_FULL_TEST) Timing HOL-Library (4 threads, 170.639s elapsed time, 405.728s cpu time, 79.823s GC time, factor 2.38) Finished HOL-Library (0:03:16 elapsed time, 0:07:24 cpu time, factor 2.26) Building Datatype_Order_Generator ... Datatype_Order_Generator: theory HashCode Datatype_Order_Generator: theory Derive_Manager Datatype_Order_Generator: theory Order_Generator Datatype_Order_Generator: theory Hash_Generator Datatype_Order_Generator: theory Countable_Generator Datatype_Order_Generator: theory Derive Datatype_Order_Generator: theory Derive_Examples Timing Datatype_Order_Generator (4 threads, 76.113s elapsed time, 113.881s cpu time, 22.905s GC time, factor 1.50) Finished Datatype_Order_Generator (0:01:40 elapsed time, 0:02:36 cpu time, factor 1.56) Building Kleene_Algebra ... Kleene_Algebra: theory Bit_Operations Kleene_Algebra: theory Misc_Typedef Kleene_Algebra: theory Misc_Numeric Kleene_Algebra: theory Signatures Kleene_Algebra: theory Dioid Kleene_Algebra: theory Bit_Representation Kleene_Algebra: theory Bit_Int Kleene_Algebra: theory Bool_List_Representation Kleene_Algebra: theory Word Kleene_Algebra: theory Dioid_Models Kleene_Algebra: theory Kleene_Algebras Kleene_Algebra: theory Action_Algebra Kleene_Algebra: theory Omega_Algebra Kleene_Algebra: theory Matrix Kleene_Algebra: theory Kleene_Algebra_Models Kleene_Algebra: theory Action_Algebra_Models Timing Kleene_Algebra (4 threads, 30.233s elapsed time, 96.144s cpu time, 6.703s GC time, factor 3.18) Finished Kleene_Algebra (0:00:48 elapsed time, 0:02:06 cpu time, factor 2.62) Building HOL-UTP ... HOL-UTP: theory List_extra HOL-UTP: theory Multi_Elem HOL-UTP: theory Product_ord HOL-UTP: theory Lattices_extra HOL-UTP: theory Map_Extra HOL-UTP: theory Fset HOL-UTP: theory Fmap HOL-UTP: theory Library_extra HOL-UTP: theory utp_common HOL-UTP: theory utp_names HOL-UTP: theory utp_value HOL-UTP: theory utp_event HOL-UTP: theory utp_var HOL-UTP: theory utp_sorts HOL-UTP: theory utp_synonyms HOL-UTP: theory utp_binding HOL-UTP: theory utp_rename HOL-UTP: theory utp_pred HOL-UTP: theory utp_pred_tac HOL-UTP: theory utp_unrest HOL-UTP: theory utp_expr HOL-UTP: theory utp_expr_tac HOL-UTP: theory utp_list HOL-UTP: theory utp_rename_laws HOL-UTP: theory utp_rel HOL-UTP: theory utp_fset HOL-UTP: theory utp_poly_value HOL-UTP: theory utp_poly_var HOL-UTP: theory utp_rel_tac HOL-UTP: theory utp_poly_expr HOL-UTP: theory utp_xrel_tac HOL-UTP: theory utp_subst_laws HOL-UTP: theory utp_pred_laws HOL-UTP: theory utp_alpha_pred HOL-UTP: theory utp_poly HOL-UTP: theory utp_pred_parser HOL-UTP: theory utp_rel_laws HOL-UTP: theory utp_poly_laws HOL-UTP: theory utp_subst_tac HOL-UTP: theory utp_theory HOL-UTP: theory utp_lattice HOL-UTP: theory utp_assert HOL-UTP: theory utp_recursion HOL-UTP: theory utp_refine_laws HOL-UTP: theory utp_iteration HOL-UTP: theory utp_hoare HOL-UTP: theory utp_wp HOL-UTP: theory utp_core HOL-UTP: theory utp_base

HOL-UTP FAILED (see also C:\Users\pgl\Desktop\Isabelle2013\heaps\polyml-5.5.0_x86-cygwin\log\HOL-UTP)

* The SMT solver Z3 is not activated. To activate it, set * the environment variable "Z3_NON_COMMERCIAL" to "yes", * and restart the Isabelle system. * See also "/cygdrive/c/Users/pgl/Desktop/Isabelle2013/contrib/z3-3.2/etc/settings" * At command "apply" (line 285 of "~~/src/utp-isabelle/theories/utils/Library_extra/Map_Extra.thy") * The SMT solver Z3 is not activated. To activate it, set * the environment variable "Z3_NON_COMMERCIAL" to "yes", * and restart the Isabelle system. * See also "/cygdrive/c/Users/pgl/Desktop/Isabelle2013/contrib/z3-3.2/etc/settings" * At command "apply" (line 258 of "~~/src/utp-isabelle/theories/utils/Library_extra/Map_Extra.thy") * The SMT solver Z3 is not activated. To activate it, set * the environment variable "Z3_NON_COMMERCIAL" to "yes", * and restart the Isabelle system. * See also "/cygdrive/c/Users/pgl/Desktop/Isabelle2013/contrib/z3-3.2/etc/settings" * At command "apply" (line 166 of "~~/src/utp-isabelle/theories/utils/Library_extra/Map_Extra.thy") * The SMT solver Z3 is not activated. To activate it, set * the environment variable "Z3_NON_COMMERCIAL" to "yes", * and restart the Isabelle system. * See also "/cygdrive/c/Users/pgl/Desktop/Isabelle2013/contrib/z3-3.2/etc/settings" * At command "apply" (line 72 of "~~/src/utp-isabelle/theories/utils/Library_extra/Map_Extra.thy") HOL-UTP-THY CANCELLED HOL-UTP-CML CANCELLED Unfinished session(s): HOL-UTP, HOL-UTP-CML, HOL-UTP-THY

Problem is probably that I also need to fetch Z3, but the error message could definitely be improved...

[joey-coleman]

Comment by ldcouto, 2013-09-26 19:30:47.929000:

• status: open --> accepted
• assigned_to: Richard Payne

[joey-coleman]

Comment by lausdahl, 2013-11-18 15:57:44.586000:

• Module: --> proof

[joey-coleman]

Comment by richardpayne, 2013-11-18 16:24:52.182000:

New theorem prover setup procedure will stop this occurring.

[joey-coleman]

Comment by richardpayne, 2013-11-18 16:25:16.353000:

• status: accepted --> closed