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
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
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:
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.
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.
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