[isabelle-dev] datatype_new problem
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Tue Jul 15 00:37:29 CEST 2014
> consider the following datatype specification
> datatype_new 'f f =
> F1 'f 'f 'f 'f |
> F2 'f 'f 'f 'f
> (which takes about 1 second with Isabelle2014-RC0) does not terminate within a few minutes anymore.
> I did not have time to do a proper bisect until now. Maybe you could have a look ;)
Please do not waste your time bisecting things that we broke! ;)
It was easy for me to track down the problem. The tactic for the new property "rel_cases" does not terminate on this example. I have disabled the generation of the property altogether (change 6bb3dd7f8097) until this is fixed.
As a workaround (for this and future tactic issues), you can always try to "declare [[quick_and_dirty = true]]" right before and disable the option right afterward (and let us know of course!).
Sorry for the trouble.
More information about the isabelle-dev