[isabelle-dev] Towards datatype_new ~> datatype

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Wed Sep 10 18:16:30 CEST 2014


Am 09.09.2014 um 20:30 schrieb Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>:

> So don't worry if your favorite theory gets some "datatype_new"s in them. They will go away soon enough.

I would like to add one thing: I am of course keeping an eye on Isatest and Testboard. As usual, I will only push changes to Isabelle that pass the "makeall" test -- but it might be that some Isatest or AFP tests sometimes will fail. For example, there have been some timeouts with "HOL-Nominal-Examples" lately in connection with my changes. Because of the big pipeline of patches I am playing with, the nondeterministic nature of some of the failures, and the complicated dependencies of AFP entries upon each other, it may take a few days before I solve the problems. Don't worry, they are on my radar.

Jasmin




More information about the isabelle-dev mailing list