Re: [isabelle] jEdit apparantly proves False

On 11/22/2013 10:53 AM, Makarius wrote:
The situation is indeed so bad that I am about to produce a new stable release of Isabelle2013-2 soon: the first (and probably only) release candidate is scheduled for Sun 24-Nov-2013 and the final release for Sun 01-Dec-2013.

So if there is anything else to report, there are a few days left to do it in a relaxed manner. Changing a formal release candidate next week requires more weight and gravity. The current state of affairs can be seen here


In general, I've seen that with Isabelle2013-1 and the RC versions, a poly.exe process will many times get started and never get terminated, and end up running at about 95% of the CPU.

It has been Sledgehammer that I've mainly associated that with, but today, I was using the command "export_code" in a simple theory, which I include below.

With Isabelle2013, rarely did processes get started that weren't terminated.

With the theory I show below, the IDE froze up while I was working with it, after which I restarted jEdit. I made some changes, which involved export_code, and then I closed the file, after which I noticed that the CPU was running at about 95%.

After I closed jEdit, a bunch of processes terminated, including a poly.exe, but these 4 processes were still running:


On 11/11/2013 5:24 AM, Makarius wrote:
There's also no persistence in the "Provers" field.

The persistence is in the history of the text field. This is also useful to "park" several sets of options that are commonly used.

That's what I was talking about. In the the drop-down box, there's the string "Previously entered strings:". There's nothing ever there except for that message.


theory i131123a__scala_hask_for_meta_obj_imps
imports Complex_Main
definition metaImp :: "prop => prop => prop" where
  "metaImp x y == (PROP x ==> PROP y)"

definition objToMetaImp :: "bool => bool => prop" where
  "objToMetaImp x y == (x ==> y)"

definition objImp :: "bool => bool => bool" where
  "objImp x y == (x --> y)"

export_code metaImp objToMetaImp objImp in Scala file "i131123a.scala"
export_code metaImp objToMetaImp objImp in Haskell file "."

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