Re: [isabelle-dev] HOL-Probability broken
I’ve pushed a correction to that particular problem. I’ve no time to verify that there are no further problems. Sorry again. Larry On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote: In Isabelle/cd945dc13bec HOL-Probability is broken: *** Now trying to infer coercions globally. *** *** Coercion inference failed: *** uncomparable types in type list *** *** Cannot fulfil subtype constraints: *** ??'a : ereal from function application *** \integral\^sup+ x. ereal (x ^ k * exp (- x)) * ***indicator {0::??'i..} x ***\partiallborel = *** fact k *** ereal : ereal from function application *** op = *** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) * *** indicator {0::??'h..} x *** \partiallborel) *** nat = ??'a : ??'b = ??'c from function application *** fact::??'b = ??'c *** At command lemma (line 116 of ~~/src/HOL/Probability/Distributions.thy) The problem might be an untested merge by Larry, but I did not make more detailed tests to prove that hypothesis. What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show any activity nor results of testing. Maybe the mira service is down? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Probability broken
In Isabelle/cd945dc13bec HOL-Probability is broken: *** Now trying to infer coercions globally. *** *** Coercion inference failed: *** uncomparable types in type list *** *** Cannot fulfil subtype constraints: *** ??'a : ereal from function application *** \integral\^sup+ x. ereal (x ^ k * exp (- x)) * ***indicator {0::??'i..} x ***\partiallborel = *** fact k *** ereal : ereal from function application *** op = *** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) * *** indicator {0::??'h..} x *** \partiallborel) *** nat = ??'a : ??'b = ??'c from function application *** fact::??'b = ??'c *** At command lemma (line 116 of ~~/src/HOL/Probability/Distributions.thy) The problem might be an untested merge by Larry, but I did not make more detailed tests to prove that hypothesis. What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show any activity nor results of testing. Maybe the mira service is down? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Probability broken
Sorry, I don’t know how that one slipped through. I test on my own machine. Larry On 17 Mar 2015, at 17:22, Makarius makar...@sketis.net wrote: In Isabelle/cd945dc13bec HOL-Probability is broken: *** Now trying to infer coercions globally. *** *** Coercion inference failed: *** uncomparable types in type list *** *** Cannot fulfil subtype constraints: *** ??'a : ereal from function application *** \integral\^sup+ x. ereal (x ^ k * exp (- x)) * ***indicator {0::??'i..} x ***\partiallborel = *** fact k *** ereal : ereal from function application *** op = *** (\integral\^sup+ x. ereal (x ^ k * exp (- x)) * *** indicator {0::??'h..} x *** \partiallborel) *** nat = ??'a : ??'b = ??'c from function application *** fact::??'b = ??'c *** At command lemma (line 116 of ~~/src/HOL/Probability/Distributions.thy) The problem might be an untested merge by Larry, but I did not make more detailed tests to prove that hypothesis. What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show any activity nor results of testing. Maybe the mira service is down? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev