[isabelle-dev] buildall inconsistency

[Manuel Eberl]

Yes, this has something to do with my ongoing changes to Euclidean Rings 
and related stuff. Everything in the distribution already works again 
and, as for the AFP, I'm on it.

I've removed all of the redundant facts in Euclidean_Algorithm and moved 
all the facts that are not specific to Euclidean Rings to semiring_gcd 
and ring_gcd. I also took care of the appropriate subclass instances and 
fixed code generation for Gcd/Lcm.

Most importantly, I also adapted all the AFP entries that use the 
polynomial GCD to work with the GCD from Euclidean_Algorithm instead of 
their own instances.

We should be able to move Euclidean_Algorithm out of Number_Theory and 
into the main HOL soon.


Cheers,

Manuel


On 28/02/16 13:00, Florian Haftmann wrote:
> (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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>