[isabelle-dev] buildall inconsistency

[Florian Haftmann]

(This is real, not an accidental build environment dropout)

isabelle: beb3e6c1fa5a tip
afp: 26bbd9a85c0c tip

> Building Pre_Polynomial_Factorization ...
> Building Sqrt_Babylonian ...
> Running AODV ...
> Running Hermite ...
> Running Impossible_Geometry ...
> Running Perfect-Number-Thm ...
> 
> Perfect-Number-Thm FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Perfect-Number-Thm)
> val it = (): unit
> Loading theory "Primes" (required by "Perfect" via "Sigma" via "PerfectBasics")
> Loading theory "Infinite_Set" (required by "Perfect" via "Sigma")
> ### theory "Infinite_Set"
> ### 2.227s elapsed time, 6.440s cpu time, 1.968s GC time
> ### theory "Primes"
> ### 2.278s elapsed time, 6.752s cpu time, 2.000s GC time
> Loading theory "Exponent" (required by "Perfect" via "Sigma" via "PerfectBasics")
> ### theory "Exponent"
> ### 0.329s elapsed time, 1.756s cpu time, 0.148s GC time
> Loading theory "PerfectBasics" (required by "Perfect" via "Sigma")
> ### theory "PerfectBasics"
> ### 0.159s elapsed time, 0.844s cpu time, 0.056s GC time
> Loading theory "Sigma" (required by "Perfect")
> ### theory "Sigma"
> ### 0.559s elapsed time, 2.836s cpu time, 0.204s GC time
> Loading theory "Perfect"
> ### theory "Perfect"
> ### 0.161s elapsed time, 0.724s cpu time, 0.076s GC time
> *** Undefined fact: "division_decomp_nat" (line 196 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "by" (line 196 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> ### Metis: Unused theorems: "Groups.ab_semigroup_add_class.add.commute", "Groups.ab_semigroup_add_class.add.left_commute"
> ### Metis: Unused theorems: "Groups.ab_semigroup_add_class.add.commute", "Groups.ab_semigroup_add_class.add.left_commute"
> *** Undefined fact: "coprime_exp_nat" (line 163 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "apply" (line 163 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** Undefined fact: "coprime_exp_nat" (line 203 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "by" (line 203 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> ### Ignoring duplicate rewrite rule:
> ### ?a1 dvd ?y \<Longrightarrow> ?a1 * (?y div ?a1) \<equiv> ?y
> *** Undefined fact: "coprime_exp_nat" (line 203 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "by" (line 203 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** Undefined fact: "coprime_exp_nat" (line 163 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "apply" (line 163 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** Undefined fact: "division_decomp_nat" (line 196 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> *** At command "by" (line 196 of "/mnt/home/haftmann/data/tum/afp/master/thys/Perfect-Number-Thm/Sigma.thy")
> Running QR_Decomposition ...
> 
> Impossible_Geometry FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Impossible_Geometry)
>   minus_point == minus :: point \<Rightarrow> point \<Rightarrow> point
>   plus_point == plus :: point \<Rightarrow> point \<Rightarrow> point
> instantiation
>   point :: metric_space
>   dist_point == dist :: point \<Rightarrow> point \<Rightarrow> real
>   uniformity_point == uniformity :: (point \<times> point) filter
>   open_point == open :: point set \<Rightarrow> bool
> Proofs for inductive predicate(s) "radical_sqrtp"
>   Proving monotonicity ...
>   Proving the introduction rules ...
>   Proving the elimination rules ...
>   Proving the induction rule ...
>   Proving the simplification rules ...
> Found termination order: "size <*mlex*> {}"
> Found termination order: "size <*mlex*> {}"
> Found termination order: "size <*mlex*> {}"
> Found termination order: "{}"
> Proofs for inductive predicate(s) "constructiblep"
>   Proving monotonicity ...
>   Proving the introduction rules ...
>   Proving the elimination rules ...
>   Proving the induction rule ...
>   Proving the simplification rules ...
> ### theory "Impossible_Geometry"
> ### 7.730s elapsed time, 17.180s cpu time, 3.876s GC time
> ### Metis: Unused theorems: "local.a", "local.d"
> ### Metis: Unused theorems: "local.b", "local.e"
> *** Undefined fact: "gcd_exp_int" (line 1285 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1285 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> ### Metis: Unused theorems: "local.hypsp_2", "local.hypsp_3"
> *** Undefined fact: "gcd_exp_int" (line 1336 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1336 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** Undefined fact: "coprime_exp_int" (line 1365 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1365 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** Undefined fact: "coprime_exp_int" (line 1365 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1365 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** Undefined fact: "gcd_exp_int" (line 1336 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1336 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** Undefined fact: "gcd_exp_int" (line 1285 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> *** At command "by" (line 1285 of "/mnt/home/haftmann/data/tum/afp/master/thys/Impossible_Geometry/Impossible_Geometry.thy")
> Running Encodability_Process_Calculi ...
> 
> Sqrt_Babylonian FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Sqrt_Babylonian)
>> val it = (): unit
> Loading theory "Sqrt_Babylonian_Auxiliary" (required by "NthRoot_Impl")
> ### theory "Sqrt_Babylonian_Auxiliary"
> ### 2.780s elapsed time, 7.608s cpu time, 2.004s GC time
> Loading theory "NthRoot_Impl"
> locale fixed_root =
>   fixes p :: "nat" 
>     and pm :: "nat" 
>   assumes "fixed_root p pm"
> locale fixed_root =
>   fixes p :: "nat" 
>     and pm :: "nat" 
>   assumes "fixed_root p pm"
> ### theory "NthRoot_Impl"
> ### 2.063s elapsed time, 6.552s cpu time, 1.112s GC time
> Loading theory "Sqrt_Babylonian"
> locale sqrt_approximation =
>   fixes \<epsilon> :: "'a" 
>     and n :: "'a" 
>   assumes "sqrt_approximation \<epsilon> n"
> ### theory "Sqrt_Babylonian"
> ### 0.812s elapsed time, 4.332s cpu time, 0.184s GC time
> ### Ignoring duplicate rewrite rule:
> ### of_int (?z1 ^ ?n1) \<equiv> of_int ?z1 ^ ?n1
> *** Undefined fact: "coprime_exp_int" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")

> *** At command "by" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> (log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
> (real_of_int (int b ^ ss) < real_of_int x)
> "(215912063945802350977 / 152672884556058511392,
>   1104427674243920646305299201 / 23309009678667569523128057147486993777664,
>   True)"
>   :: "rat \<times> rat \<times> bool"
> *** Undefined fact: "coprime_exp_int" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> *** At command "by" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> Real_Impl CANCELLED
> Running Probabilistic_Noninterference ...
> 
> Hermite FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Hermite)
>       "\<And>b a c.
>           b \<noteq> (0::'a) \<Longrightarrow>
>           (a + c * b) div b = c + a div b"
>     and
>     "div_mult_mult1":
>       "\<And>c a b.
>           c \<noteq> (0::'a) \<Longrightarrow> c * a div (c * b) = a div b"
> class semiring_div = div + algebraic_semidom +
>   assumes "mod_div_equality": "\<And>a b. a div b * b + a mod b = a"
>     and "div_by_0": "\<And>a. a div (0::'a) = (0::'a)"
>     and "div_0": "\<And>a. (0::'a) div a = (0::'a)"
>     and
>     "div_mult_self1":
>       "\<And>b a c.
>           b \<noteq> (0::'a) \<Longrightarrow>
>           (a + c * b) div b = c + a div b"
>     and
>     "div_mult_mult1":
>       "\<And>c a b.
>           c \<noteq> (0::'a) \<Longrightarrow> c * a div (c * b) = a div b"
> ### theory "Hermite"
> ### 10.324s elapsed time, 29.832s cpu time, 4.196s GC time
> Loading theory "Hermite_IArrays"
> ### theory "Hermite_IArrays"
> ### 1.745s elapsed time, 6.540s cpu time, 1.052s GC time
> "IArray [IArray [1, 44, 57], IArray [0, 108, 52], IArray [0, 0, 63]]"
>   :: "int iarray iarray"
> "[[1, 44, 57], [0, 108, 52], [0, 0, 63]]"
>   :: "int list list"
> "IArray [IArray [1, 44, 57], IArray [0, 108, 52], IArray [0, 0, 63]]"
>   :: "int iarray iarray"
> "[[[:1:], [:- (44 / 89), 31 / 89, - (68 / 89), 137 / 89, 40 / 89:]],
>   [0, [:- (2 / 5), 4 / 5, 4, 22 / 5, 24 / 5, 1:]]]"
>   :: "real poly list list"
> "IArray
>   [IArray [[:1:], [:- (44 / 89), 31 / 89, - (68 / 89), 137 / 89, 40 / 89:]],
>    IArray [0, [:- (2 / 5), 4 / 5, 4, 22 / 5, 24 / 5, 1:]]]"
>   :: "real poly iarray iarray"
> *** Undefined fact: "gcd_poly.simps" (line 37 of "/mnt/home/haftmann/data/tum/afp/master/thys/Hermite/Hermite.thy")
> *** At command "by" (line 36 of "/mnt/home/haftmann/data/tum/afp/master/thys/Hermite/Hermite.thy")
> 
> Pre_Polynomial_Factorization FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/Pre_Polynomial_Factorization)
> registered mat in class set_impl
> use dlist as set_impl for type vec
> registered vec in class set_impl
> use None as trivial implementation of cenum for type mat
> registered mat in class cenum
> use None as trivial implementation of cenum for type vec
> registered vec in class cenum
> ### theory "Matrix_IArray_Impl"
> ### 5.297s elapsed time, 16.428s cpu time, 2.408s GC time
> ### theory "Gauss_Jordan"
> ### 6.924s elapsed time, 20.880s cpu time, 5.188s GC time
> Loading theory "Gauss_Jordan_IArray_Impl"
> ### theory "Gauss_Jordan_IArray_Impl"
> ### 3.884s elapsed time, 15.888s cpu time, 3.660s GC time
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>\<And>i j.
> ###             \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
> ###             \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
> ###  dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
> ### \<Longrightarrow> ?A = ?B
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>\<And>i j.
> ###             \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
> ###             \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
> ###  dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
> ### \<Longrightarrow> ?A = ?B
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>\<And>i j.
> ###             \<lbrakk>i < dim\<^sub>r ?B; j < dim\<^sub>c ?B\<rbrakk>
> ###             \<Longrightarrow> ?A $$ (i, j) = ?B $$ (i, j);
> ###  dim\<^sub>r ?A = dim\<^sub>r ?B; dim\<^sub>c ?A = dim\<^sub>c ?B\<rbrakk>
> ### \<Longrightarrow> ?A = ?B
> "\<zero>\<^sub>v
>   6 |\<^sub>v 1 \<mapsto> (2::'a) |\<^sub>v 2 \<mapsto> (3::'a)"
>   :: "'a vec"
> (log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
> (real_of_int (int b ^ ss) < real_of_int x)
> "\<zero>\<^sub>m 6
>   4 |\<^sub>m (1, 3) \<mapsto> (2::'a) |\<^sub>m (2, 1) \<mapsto> (3::'a)"
>   :: "'a mat"
> "(215912063945802350977 / 152672884556058511392,
>   1104427674243920646305299201 / 23309009678667569523128057147486993777664,
>   True)"
>   :: "rat \<times> rat \<times> bool"
> *** Undefined fact: "coprime_exp_int" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> *** At command "by" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> Polynomial_Factorization CANCELLED
> Pre_Algebraic_Numbers CANCELLED
> Algebraic_Numbers CANCELLED
> 
> QR_Decomposition FAILED
> (see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/QR_Decomposition)
>    \<And>b. b \<in> ?C - ?B \<Longrightarrow> ?h b = (0::?'a);
>    setsum ?g ?C = setsum ?h ?C\<rbrakk>
>   \<Longrightarrow> setsum ?g ?A = setsum ?h ?B
> "None"
>   :: "(real list \<times> real list set) option"
> "Some ([4, - 3, 0], {[1, - 1, 1]})"
>   :: "(real list \<times> real list set) option"
> "Some
>   ([63 / 5, 57 / 5, 0, 0], {[2, 2, 1, 0], [- (26 / 5), - (24 / 5), 0, 1]})"
>   :: "(real list \<times> real list set) option"
> "{False, True}"
>   :: "bool set"
> "{False, True}"
>   :: "bool set"
> \<lbrakk>finite {p. 0 \<le> p \<and> nat 0 < f p};
>  \<And>p.
>     \<lbrakk>0 \<le> p; nat 0 < f p\<rbrakk>
>     \<Longrightarrow> prime (nat p)\<rbrakk>
> \<Longrightarrow> prime_factors
>                    (\<Prod>x\<in>{p. 0 \<le> p \<and> nat 0 < f p}.
>                       x ^ f x) =
>                   {p. 0 \<le> p \<and> nat 0 < f p}
> "{a\<^sub>1, a\<^sub>2}"
>   :: "Enum.finite_2 set"
> "op *s"
>   :: "'a \<Rightarrow> ('a, 'b) vec \<Rightarrow> ('a, 'b) vec"
> "op *\<^sub>R"
>   :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
> (log (real b) (real_of_int (int b ^ ss)) < log (real b) (real_of_int x)) =
> (real_of_int (int b ^ ss) < real_of_int x)
> "{a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"
>   :: "Enum.finite_5 set"
> "{a\<^sub>1, a\<^sub>2}"
>   :: "Enum.finite_2 set"
> "{[- 10, 5, 1, 0]}"
>   :: "real list set"
> "{[- (1 / 4), - 1, - (3 / 4), 1]}"
>   :: "real list set"
> *** Undefined fact: "coprime_exp_int" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> *** At command "by" (line 1007 of "/mnt/home/haftmann/data/tum/afp/master/thys/Sqrt_Babylonian/NthRoot_Impl.thy")
> Unfinished session(s): Algebraic_Numbers, Hermite, Impossible_Geometry, Perfect-Number-Thm, Polynomial_Factorization, Pre_Algebraic_Numbers, Pre_Polynomial_Factorization, QR_Decomposition, Real_Impl, Sqrt_Babylonian