Re: [isabelle] Isabelle2016-RC0: cvc4 crashing



Dear Eugene,

> But now before I can get back to what I was doing and report on whether CVC4 is still crashing,

Please let us know how this goes. Regardless, the next release candidate will likely feature a new version of CVC4.

> I need to know what the new warning "Not a proper equation" means in a
> datatype definition as follows (also attached):

Thank you for your report. In short, the code generator is now more verbose, and the "datatype" package interacts with it. I have a solution locally to get rid of the warning that is likely to be part of the next release candidate.

> Another issue I noticed: JEdit now forcibly resets the indentations of lines
> with keywords such as "locale" when I type the keyword, or, what is even
> more irritating, when I type ENTER at the end of the line.  I think this
> new behavior is fairly disruptive of the typing habits I have established
> to this point.

I guess this is for Makarius to answer.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.