Re: [isabelle] Isabelle2016-RC0: cvc4 crashing



You have embarrassed me into attempting to merge my stuff and try Isabelle2016-1-RC0.
But now before I can get back to what I was doing and report on whether CVC4 is still
crashing, I need to know what the new warning "Not a proper equation" means in a
datatype definition as follows (also attached):

theory Barf
imports Main Category
begin

  locale foo =
    fixes X
    assumes "X = X"

  context foo
  begin

    datatype (discs_sels) 't "term" =
      C
    | T "'t term * 't term"

end

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.

							- Gene Stark



On 10/26/2016 07:45 AM, Makarius wrote:
> On 26/10/16 12:42, Eugene W. Stark wrote:
>> CVC4 still crashes regularly with Isabelle2016 on Ubuntu 16.04 LTS.
>> For some reason it seems to still be useful, though.  I believe this
>> is because (as surmised earlier in this thread) the crashing seems to
>> occur when Isabelle kills a no-longer-needed CVC4 process, not during
>> actual useful work.
> 
> Did you try Isabelle2016-1-RC0 from
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC0 already?
> 
> There is now also a daily snapshot at http://isabelle.in.tum.de/devel --
> it will quickly converge to Isabelle2016-1-RC1 at the end of the week.
> 
> 
> 	Makarius
> 
> 

theory Barf
imports Main Category
begin

  locale foo =
    fixes X
    assumes "X = X"

  context foo
  begin

    datatype (discs_sels) 't "term" =
      C
    | T "'t term * 't term"

end


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