Re: [isabelle] Strange interaction between Rewrite and Adhoc_Overloading



> It is probably better to move Adhoc_Overloading.thy to
> ~~/src/HOL/Library and make it import Main. (I am in the process to try
> this change of Isabelle + AFP.)

This change (Isabelle/81d90f830f99) broke HOLCF-Prelude in the AFP (see
attachment).
--- Begin Message ---
The build for the session
  HOLCF-Prelude,
belonging to the AFP entry
  HOLCF-Prelude
failed.

You are receiving this mail because you are the maintainer of that AFP
entry.

The following information might help you with resolving the problem.

Build log:    https://ci.isabelle.systems/jenkins/job/isabelle-repo-afp/1615/
Isabelle ID:  81d90f830f99
AFP ID:       8c085909633b
Timeout?      false
Exit code:    2

Last 50 lines from stdout (if available):

(see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.7.1_x86_64-linux/log/HOLCF-Prelude)
###               ("_Cons_section"))
###             ("\<^const>Data_List.list.Nil_cont_syntax"))))
###       ("_Coll" ("_pattern" ("_position" f) ("_position" xs))
###         ("\<^const>HOL.eq" ("_position" f)
###           ("_applC" ("_position" abstract_list) ("_position" xs)))))))
### ("\<^const>Pure.all_binder" ("_position" v)
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Set.member"
###       ("_tuple"
###         ("\<^const>Cfun.cfun.Rep_cfun" ("_position" down') ("_position" v))
###         ("_tuple_arg"
###           ("\<^const>Cfun.cfun.Rep_cfun"
###             ("\<^const>Cfun.cfun.Rep_cfun"
###               ("\<^const>Cfun.cfun.Rep_cfun" ("_position" down')
###                 ("_position" v))
###               ("\<^const>Data_List.list.Cons_cont_syntax"))
###             ("\<^const>Data_List.list.Nil_cont_syntax"))))
###       ("_Coll" ("_pattern" ("_position" f) ("_position" xs))
###         ("\<^const>HOL.eq" ("_position" f)
###           ("_applC" ("_position" abstract_list) ("_position" xs)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Introduced fixed type variable(s): 'c, 'd in "p__"
### Introduced fixed type variable(s): 'c, 'd in "p__"
### Rule already declared as introduction (intro)
### (\<And>x. f x = g x) \<Longrightarrow> f = g
### Rule already declared as introduction (intro)
### (\<And>x. f x = g x) \<Longrightarrow> f = g
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Prelude/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Prelude/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "HOLCF-Prelude.Fibs" (unresolved "HOLCF-Prelude.Definedness")
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ \<rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  Rep_cfun ::
***   (?'a \<rightarrow> ?'b) \<Rightarrow> ?'a \<Rightarrow> ?'b
*** Operand:   (!) :: ?'c List.list \<Rightarrow> nat \<Rightarrow> ?'c
*** 
*** At command "lemma" (line 199 of "~~/afp/thys/HOLCF-Prelude/Definedness.thy")

Last 50 lines from stderr (if available):

Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Prelude
Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Prelude/document.pdf
Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/HOLCF-Prelude/outline.pdf


--- End Message ---


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.