Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error in build after trivial change

Email Gateway (Aug 23 2022 at 08:14):

From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Hello,

I was doing a small and rather trivial change in the library, and the
test build fails with errors I can't link to the change I made; however
without the change the build works fine. The change I made and the
error message are given below. Does anybody have an idea what might be
going on?

--- change to the library ---

~/isabelle$ hg diff
diff -r 5385de42f9f4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy Tue Jan 28 14:59:54 2020 +0000
+++ b/src/HOL/Euclidean_Division.thy Tue Jan 28 21:32:28 2020 +0100
@@ -11,8 +11,10 @@

subsection \<open>Euclidean (semi)rings with explicit division and
remainder\<close>

-class euclidean_semiring = semidom_modulo +
+class pre_euclidean_size =
fixes euclidean_size :: "'a \<Rightarrow> nat"
+
+class euclidean_semiring = pre_euclidean_size + semidom_modulo +
assumes size_0 [simp]: "euclidean_size 0 = 0"
assumes mod_size_less:
"b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) <
euclidean_size b"

--- build fail ---

~/isabelle$ ./bin/isabelle build -j2 -o threads=3 HOL-
Computational_Algebra
Building HOL ...
Finished HOL (0:04:53 elapsed time, 0:11:44 cpu time, factor 2.40)
Building HOL-Library ...
Finished HOL-Library (0:03:37 elapsed time, 0:09:00 cpu time, factor
2.49)
Running HOL-Computational_Algebra ...
HOL-Computational_Algebra FAILED
(see also /home/christian/.isabelle/heaps/polyml-5.8.1_x86_64_32-
linux/log/HOL-Computational_Algebra)

\<Prod>x\<in>?A1. ?y1 \<equiv> ?y1 ^ card ?A1

Ignoring duplicate rewrite rule:

fps_of_poly ?p1 $ ?n1 \<equiv> coeff ?p1 ?n1

Ignoring duplicate rewrite rule:

fps_of_poly 0 \<equiv> 0

Ignoring duplicate rewrite rule:

fps_of_poly 0 \<equiv> 0

Ignoring duplicate rewrite rule:

fps_of_poly 1 \<equiv> 1

Ignoring duplicate rewrite rule:

fps_of_poly (numeral ?n1) \<equiv> numeral ?n1

Ignoring duplicate rewrite rule:

fps_of_poly [:0::?'a1, 1::?'a1:] \<equiv> fps_X

Ignoring duplicate rewrite rule:

fps_of_poly (pCons ?c1 ?p1) \<equiv> fps_const ?c1 + fps_of_poly

?p1 * fps_X
*** Failed to load theory "HOL-
Computational_Algebra.Computational_Algebra" (unresolved "HOL-
Computational_Algebra.Polynomial_Factorial")
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and
"nat"

*** Type error in application: incompatible operand type

*** Operator: class.normalization_euclidean_semiring_multiplicative ::
*** (??'a \<Rightarrow> nat)
*** \<Rightarrow> (??'a \<Rightarrow> ??'a \<Rightarrow> ??'a)
*** \<Rightarrow> (??'a \<Rightarrow> ??'a
\<Rightarrow> ??'a)
*** \<Rightarrow> (??'a
*** \<Rightarrow> ??'a \<Rightarrow> ??'a)
*** \<Rightarrow> ??'a
*** \<Rightarrow> (??'a
*** \<Rightarrow> ??'a \<Rightarrow>
??'a)
*** \<Rightarrow> ??'a
*** \<Rightarrow> (??'a \<Rightarrow> ??'a \<Rightarrow>
??'a)
*** \<Rightarrow> (??'a \<Rightarrow> ??'a)
*** \<Rightarrow> (??'a \<Rightarrow> ??'a) \<Rightarrow> bool
*** Operand: (div) :: ??'a \<Rightarrow> ??'a \<Rightarrow> ??'a

*** Coercion Inference:

*** Local coercion insertion on the operand failed:
*** No coercion known for type constructors: "fun" and "nat"
*** At command "show" (line 400 of
"~~/src/HOL/Computational_Algebra/Polynomial_Factorial.thy")
Unfinished session(s): HOL-Computational_Algebra
0:09:23 elapsed time, 0:22:25 cpu time, factor 2.39

Email Gateway (Aug 23 2022 at 08:14):

From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear Christian,

before the change, Isabelle's type inference inferred
"euclidean_semiring" whenever "euclidean_size" was used, but now only
"pre_euclidean_size". And unfortunately, some library statements depend
on the type inference.

BTW: I'd like to support your change, which is in line of syntactic
classes plus, times, etc. Following the convention, the class could be
called "euclidean_size".

Best regards,
Akihisa

Last updated: Nov 21 2024 at 12:39 UTC