Re: [isabelle-dev] HOL-Probability broken
On Wed, 18 Mar 2015, Larry Paulson wrote: Sorry, I overlooked this due to the many untracked files of the form *.prv. Wouldn’t it make sense to add this pattern to our .hgignore file? I've never seen such *.prv files. Where are they coming from? Normally the Isabelle source space is considered read-only. The system needs to work from a read-only file-system, even though that is never tested systematically. 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
On Tue, 17 Mar 2015, Larry Paulson wrote: I’ve pushed a correction to that particular problem. That version f41a2f77ab1b looks fine. I’ve no time to verify that there are no further problems. Sorry again. New further problems emerge in 5b762cd73a8e: total existence failure due to missing file Complex_Transcendental.thy. 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 overlooked this due to the many untracked files of the form *.prv. Wouldn’t it make sense to add this pattern to our .hgignore file? Larry On 18 Mar 2015, at 14:52, Makarius makar...@sketis.net wrote: On Tue, 17 Mar 2015, Larry Paulson wrote: I’ve pushed a correction to that particular problem. That version f41a2f77ab1b looks fine. I’ve no time to verify that there are no further problems. Sorry again. New further problems emerge in 5b762cd73a8e: total existence failure due to missing file Complex_Transcendental.thy. 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
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