Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed



On 14-08-26 11:17, Makarius wrote:
This one is already quite well-known in internal circles.

...The situation might become better again, after switching to Cygwin x86_64, but I have not tried it yet.

Makarius,

I thought there was nothing more to say about it, and I didn't want to reply just to say, "Switching to Cygwin x86_64 sounds exciting, if it works". Now I have something to add.

"Auto Methods", mysteriously, could also be putting demands on the CPU when Sledgehammer is running.

I usually enable, all together, "Auto Methods", "Auto Nitpick", and "Auto Quickcheck" and forget about them.

Today, "Auto Methods" is acting as the only culprit for what I describe, because I've enabled them one at a time for the setup I describe below. "Auto Solve direct" seems to not be a problem, because I've left it enabled, and I don't use "Auto Sledgehammer".

I attach a screenshot to show what's above where I have the cursor, and what's below. It doesn't seem like any attempts should be made to prove or disprove anything, and it's not like I have this problem all the time.

My setup for the screenshot is that I started PIDE with those 3 auto options disabled. I then enabled them, with where the cursor is shown, (I then took the time to do them one at a time, with only "Auto Methods" causing this).

The CPU goes to about 50% as shown for all four cores, and then I have to terminate. Disabling the three options is not enough.

As a final note, in repeatedly starting up, enabling "Auto Methods", disabling, and then terminating PIDE, I had problems terminating, so I rebooted.

So, on a fresh boot, I started PIDE, saw the purple bar show proving until got to the cursor position I show in the screenshot, I enabled "Auto Methods", all 4 cores started working to about 50% if the CPU, I disabled "Auto Methods", and then I had to terminate.

Regards,
GB

Attachment: 140826__Auto stuff runs CPU mysteriously.png
Description: PNG image



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