Re: [isabelle-dev] Multiset_Order
OK, currently under analysis. Am 26.03.2015 um 11:41 schrieb Jasmin Blanchette: On 26.03.2015, at 11:34, Tobias Nipkow nip...@in.tum.de wrote: *** Undefined fact: comm_monoid_diff_class.diff_cancel (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) *** At command by (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) Unfinished session(s): HOL-Library Finished at Thu Mar 26 01:54:14 CET 2015 0:09:32 elapsed time, 0:19:54 cpu time, factor 2.08 I think Florian has been tuning this recently. Yes, he (cc:d) pushed changes after mine and thereby broke the build. (His changes are older but he pushed them afterwards.) Jasmin -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Multiset_Order
http://isabelle.in.tum.de/reports/Isabelle/rev/75433c3ee203 Am 26.03.2015 um 11:42 schrieb Florian Haftmann: OK, currently under analysis. Am 26.03.2015 um 11:41 schrieb Jasmin Blanchette: On 26.03.2015, at 11:34, Tobias Nipkow nip...@in.tum.de wrote: *** Undefined fact: comm_monoid_diff_class.diff_cancel (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) *** At command by (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) Unfinished session(s): HOL-Library Finished at Thu Mar 26 01:54:14 CET 2015 0:09:32 elapsed time, 0:19:54 cpu time, factor 2.08 I think Florian has been tuning this recently. Yes, he (cc:d) pushed changes after mine and thereby broke the build. (His changes are older but he pushed them afterwards.) Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Someone messed up HOL_library/Multiset_Order
Isabelle version: devel -- hg id 034b13f4efae Test ended on: macbroy2, Thu Mar 26 13:46:35 CET 2015. HOL-Library FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.2_x86-darwin/log/HOL-Library) Output written on root.pdf (710 pages, 1552625 bytes). Transcript written on root.log. *** Undefined fact: comm_monoid_diff_class.diff_cancel (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) *** At command by (line 302 of ~~/src/HOL/Library/Multiset_Order.thy) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Someone messed up HOL_library/Multiset_Order
On 26.03.2015, at 14:00, Peter Lammich lamm...@in.tum.de wrote: Isabelle version: devel -- hg id 034b13f4efae Someone pushed a fix a few hours ago already (75433c3ee203). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
